From d6959d06869c51daa14ec95b7f4abd24e1f5ce59 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 01:52:34 +0000 Subject: [PATCH 1/2] =?UTF-8?q?feat(crypto):=20computational=20Carter?= =?UTF-8?q?=E2=80=93Wegman=20MACs=20and=20nonce-based=20MAC=20interface=20?= =?UTF-8?q?(#736)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Complete the computational Carter–Wegman MAC development for #736 (building on PR #1080 by worker-jetski-cf53d356): - Add the computational nonce-based MAC interface (`NonceMACForger`, `NonceMACScheme`, `signingPairOracle`, `sufCmaGame`, `eufCmaGame`, `SUFCMA`, `EUFCMA`, `IsOraclePPTOn` simulation certificates, and `SUFCMA → EUFCMA` / unique-tag equivalence) in `Complexity/Crypto/Computational/MAC.lean`. - Add the full adaptive multi-query nonce-based Carter–Wegman reduction (`nonceFnHandler`, `nonceSimHandler`, `reconstructPadFn`, `checkNonceSUF`, `checkNonceEUF`, `nonceStrongGame_le_max`, `prfNonceStrongGame_le`, `PseudorandomFunction.negligible_prfNonceStrongGame`) and randomized Carter–Wegman birthday + pad-resampling reduction (`randomNonceFnHandler`, `randomNonceSimHandler`, `checkRandomNonceSUF`, `randomNonceStrongGame_le`, `prfRandomNonceStrongGame_le`, `PseudorandomFunction.negligible_prfRandomNonceStrongGame`) in `Complexity/Crypto/Protocols/MAC/CarterWegman.lean`. - Add word-level `IsOraclePPT encBool` PRF distinguishers (`prfNonceToPrfDistinguisher`, `isOraclePPT_prfNonceToPrfDistinguisher`, `prfRandomNonceToPrfDistinguisher`, `isOraclePPT_prfRandomNonceToPrfDistinguisher`), package `carterWegmanNonceMAC : NonceMACScheme` and `carterWegmanRandomMAC : MACScheme` along with concrete `BitString.LinearHash` instantiations (`linearHashNonceMAC`, `linearHashRandomMAC`), and prove their quantitative and asymptotic `SUFCMA` / `EUFCMA` / `OneTimeEUFCMA` security theorems. - Add multi-query adaptive `IsOraclePPT` forger and security tests in `ComplexityTests/Crypto/CarterWegman.lean` and update `ROADMAP.md`. Closes #736 --- Complexity/Crypto/Computational/MAC.lean | 642 +++- .../Crypto/Protocols/MAC/CarterWegman.lean | 2588 ++++++++++++++++- ComplexityTests/Crypto/CarterWegman.lean | 192 +- ROADMAP.md | 5 +- 4 files changed, 3386 insertions(+), 41 deletions(-) diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean index fe7cff917e..c5834fa266 100644 --- a/Complexity/Crypto/Computational/MAC.lean +++ b/Complexity/Crypto/Computational/MAC.lean @@ -78,6 +78,12 @@ $$\Pr[\text{Forge}] \le \mathrm{Adv}_{\mathrm{PRF}}(B(\mathcal{A}), n) + 2^{-n}. ([Boneh and Shoup, Section 6.3][BonehShoup2023]). * `Cslib.Crypto.macLogHandler`, `Cslib.Crypto.macToPrfDistinguisher`: oracle logging handler and reduction turning a MAC forger into a PRF distinguisher. +* `Cslib.Crypto.NonceMACForger`, `Cslib.Crypto.NonceMACScheme`: uniform nonce-based message + authentication code (`sign : Key → Msg → Nonce → ProbComp Tag`) and adaptive forger + ([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]). +* `Cslib.Crypto.NonceMACScheme.signingPairOracle`, `sufCmaGame`, `eufCmaGame`, `SUFCMA` + (`NonceSUFCMA`), `EUFCMA` (`NonceEUFCMA`): nonce-respecting adaptive chosen-message security + experiments and predicates requiring distinct queried nonces (`(tr.map (fun e => e.1.2)).Nodup`). ## Main results @@ -114,11 +120,17 @@ $$\Pr[\text{Forge}] \le \mathrm{Adv}_{\mathrm{PRF}}(B(\mathcal{A}), n) + 2^{-n}. `Cslib.Crypto.PseudorandomFunction.eufCma_prfMAC`, `Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_prfMAC`: any secure uniform `PseudorandomFunction` yields a `SUFCMA`-, `EUFCMA`-, and `OneTimeEUFCMA`-secure `MACScheme`. +* `Cslib.Crypto.NonceMACScheme.isPPTOn_sufCmaGame`, `isPPT_sufCmaGame`, `isPPTOn_eufCmaGame`, + `isPPT_eufCmaGame`, `succProbability_eufCmaGame_le_sufCmaGame`, `SUFCMA.eufCma`, + `eval_sufCmaGame_eq_freshPair_of_unique_tag`, `sufCma_iff_eufCma_of_unique_tag`: strict PPT + certificates, quantitative / asymptotic implication from `SUFCMA` to `EUFCMA`, and unique-tag + characterizations for nonce-based MACs. ## References * [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*][BonehShoup2023], Chapter 6, - Sections 6.1–6.3 (Definitions 6.1–6.2 and Theorem 6.2). + Sections 6.1–6.3 (Definitions 6.1–6.2 and Theorem 6.2) and Chapter 7, Section 7.5 (Attack Game + 7.4). * [O. Goldreich, S. Goldwasser, S. Micali, *How to Construct Random Functions*][GGM1986]. -/ @@ -1618,4 +1630,632 @@ theorem PseudorandomFunction.oneTimeEUFCMA_prfMAC (prfMAC family hprf.polyTime).OneTimeEUFCMA := hprf.eufCma_prfMAC.oneTimeEUFCMA +/-! ### Nonce-based message authentication codes (`NonceMACScheme`, Boneh–Shoup Section 7.5) -/ + +/-- An adaptive nonce-based MAC forger receives a unary security parameter and an auxiliary word, +queries a nonce-respecting tagging oracle on encoded `(message, nonce)` pairs +(`encPair encBits encBits (msg, nonce)`), and outputs a candidate `((message, nonce), tag)` triple +([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]). -/ +abbrev NonceMACForger := + ℕ → List Bool → WordOracleComp Unit ((List Bool × List Bool) × List Bool) + +/-- A uniform symmetric nonce-based message authentication code (`NonceMACScheme`) on `msgLen n`-bit +messages and `nonceLen n`-bit nonces at security parameter `n` (both defaulting to `n`), with plain +polynomial-time length schedules, strict polynomial-time key generation and tag generation, +deterministic polynomial-time verification, and perfect completeness on supported keys, +`msgLen n`-bit messages, `nonceLen n`-bit nonces, and tags +([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]). -/ +structure NonceMACScheme where + /-- Message length authenticated at unary security parameter `n` (defaults to `n`). -/ + msgLen : ℕ → ℕ := fun n => n + /-- The message-length schedule is computable in plain polynomial time in unary. -/ + msgLen_polyTime : ComputableInPolyTime msgLen encUnary encUnary := by + exact ComputableInPolyTime.id' + /-- Nonce length required at unary security parameter `n` (defaults to `n`). -/ + nonceLen : ℕ → ℕ := fun n => n + /-- The nonce-length schedule is computable in plain polynomial time in unary. -/ + nonceLen_polyTime : ComputableInPolyTime nonceLen encUnary encUnary := by + exact ComputableInPolyTime.id' + /-- Sample a secret MAC key `sk` at unary security parameter `n`. -/ + keyGen : ℕ → ProbComp (List Bool) + /-- Compute a MAC tag on message `msg` and nonce `nonce` using the secret key `sk`. -/ + sign : List Bool → List Bool → List Bool → ProbComp (List Bool) + /-- Deterministically verify a candidate `tag` on `(msg, nonce)` under secret key `sk`. -/ + verify : List Bool → List Bool → List Bool → List Bool → Bool + /-- Key generation is uniformly strict PPT in the unary security parameter. -/ + keyGen_ppt : IsPPTOn encUnary encBits keyGen + /-- Tag generation is uniformly strict PPT in the encoded `(sk, msg, nonce)`. -/ + sign_ppt : IsPPTOn (encPair encBits (encPair encBits encBits)) encBits + (fun p => sign p.1 p.2.1 p.2.2) + /-- Verification is computable in plain polynomial time on `(sk, msg, nonce, tag)`. -/ + verify_polyTime : ComputableInPolyTime + (fun p : List Bool × List Bool × List Bool × List Bool => verify p.1 p.2.1 p.2.2.1 p.2.2.2) + (encPair encBits (encPair encBits (encPair encBits encBits))) encBool + /-- Every tag produced by `sign` on a `msgLen n`-bit message and `nonceLen n`-bit nonce under a + supported secret key at security parameter `n` is accepted by `verify`. -/ + verify_sign : ∀ n sk, sk ∈ (ProbComp.eval (keyGen n)).support → + ∀ msg, msg.length = msgLen n → + ∀ nonce, nonce.length = nonceLen n → + ∀ tag, tag ∈ (ProbComp.eval (sign sk msg nonce)).support → + verify sk msg nonce tag = true + +/-- Testing membership in a framed list of bit-string pairs is computable tidily in polynomial time. +-/ +@[fun_prop] +theorem computableTidilyInPolyTime_contains_pair {γ : Type} {encIn : γ ↪ List Bool} + {list : γ → List (List Bool × List Bool)} + {elem : γ → List Bool × List Bool} + (hlist : ComputableTidilyInPolyTime list encIn (encList (encPair encBits encBits))) + (helem : ComputableTidilyInPolyTime elem encIn (encPair encBits encBits)) : + ComputableTidilyInPolyTime (fun a => (list a).contains (elem a)) encIn encBool := by + have heq : (fun a => (list a).contains (elem a)) = + (fun a => (list a).any (fun x => elem a == x)) := by + funext a + rw [Bool.eq_iff_iff, List.contains_iff_mem, List.any_eq_true] + simp only [beq_iff_eq] + exact ⟨fun h => ⟨elem a, h, rfl⟩, fun ⟨_, h, heq⟩ => heq ▸ h⟩ + rw [heq] + exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist + (ComputableTidilyInPolyTime.beq (encB := encPair encBits encBits) + (helem.comp (ComputableTidilyInPolyTime.fst _ _)) + (ComputableTidilyInPolyTime.snd _ _)) + +/-- Testing membership in a framed list of `((msg, nonce), tag)` triples is computable tidily in +polynomial time. -/ +@[fun_prop] +theorem computableTidilyInPolyTime_contains_triple {γ : Type} {encIn : γ ↪ List Bool} + {list : γ → List ((List Bool × List Bool) × List Bool)} + {elem : γ → (List Bool × List Bool) × List Bool} + (hlist : ComputableTidilyInPolyTime list encIn + (encList (encPair (encPair encBits encBits) encBits))) + (helem : ComputableTidilyInPolyTime elem encIn + (encPair (encPair encBits encBits) encBits)) : + ComputableTidilyInPolyTime (fun a => (list a).contains (elem a)) encIn encBool := by + have heq : (fun a => (list a).contains (elem a)) = + (fun a => (list a).any (fun x => elem a == x)) := by + funext a + rw [Bool.eq_iff_iff, List.contains_iff_mem, List.any_eq_true] + simp only [beq_iff_eq] + exact ⟨fun h => ⟨elem a, h, rfl⟩, fun ⟨_, h, heq⟩ => heq ▸ h⟩ + rw [heq] + exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist + (ComputableTidilyInPolyTime.beq (encB := encPair (encPair encBits encBits) encBits) + (helem.comp (ComputableTidilyInPolyTime.fst _ _)) + (ComputableTidilyInPolyTime.snd _ _)) + +/-- Deciding `List.Nodup` on a framed list of bit strings is computable tidily in polynomial time. +-/ +@[fun_prop] +theorem computableTidilyInPolyTime_decide_nodup {γ : Type} {encIn : γ ↪ List Bool} + {list : γ → List (List Bool)} + (hlist : ComputableTidilyInPolyTime list encIn (encList encBits)) : + ComputableTidilyInPolyTime (fun a => decide (list a).Nodup) encIn encBool := by + have heq : (fun a => decide (list a).Nodup) = + (fun a => (list a).all (fun x => (list a).count x == 1)) := by + funext a + rw [Bool.eq_iff_iff, decide_eq_true_eq, List.all_eq_true, List.nodup_iff_count_le_one] + simp only [beq_iff_eq] + refine ⟨fun h x hx => ?_, fun h x => ?_⟩ + · have hle := h x + have hpos := List.count_pos_iff.mpr hx + omega + · by_cases hx : x ∈ list a + · exact (h x hx).le + · simp [List.count_eq_zero.mpr hx] + rw [heq] + exact ComputableTidilyInPolyTime.allWithInput (test := fun a x => (list a).count x == 1) + hlist (by polytime) + +/-- The unframed prefix and remaining suffix of any bit list satisfy +`2 * (unframe v).length + (dropFrame v).length ≤ v.length`. -/ +theorem length_unframe_add_dropFrame_le : + ∀ v : List Bool, 2 * (unframe v).length + (dropFrame v).length ≤ v.length + | [] | [true] => by simp [unframe, dropFrame] + | false :: v => by simp [unframe, dropFrame] + | true :: b :: v => by + have ih := length_unframe_add_dropFrame_le v + simp only [unframe, dropFrame, List.length_cons] + omega + +namespace NonceMACScheme + +attribute [program_certificate] + msgLen_polyTime nonceLen_polyTime keyGen_ppt sign_ppt verify_polyTime + +@[local fun_prop] +private theorem computableTidilyInPolyTime_msgLen_comp (M : NonceMACScheme) + {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} + (hn : ComputableTidilyInPolyTime n encIn encUnary) : + ComputableTidilyInPolyTime (fun a => M.msgLen (n a)) encIn encUnary := + M.msgLen_polyTime.tidy.comp hn + +/-- Composing `M.msgLen` with a plain polynomial-time unary parameter function is plain +polynomial-time. -/ +@[program_certificate] +theorem computableInPolyTime_msgLen_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} + {n : γ → ℕ} (hn : ComputableInPolyTime n encIn encUnary) : + ComputableInPolyTime (fun a => M.msgLen (n a)) encIn encUnary := + M.msgLen_polyTime.comp hn + +@[local fun_prop] +private theorem computableTidilyInPolyTime_nonceLen_comp (M : NonceMACScheme) + {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} + (hn : ComputableTidilyInPolyTime n encIn encUnary) : + ComputableTidilyInPolyTime (fun a => M.nonceLen (n a)) encIn encUnary := + M.nonceLen_polyTime.tidy.comp hn + +/-- Composing `M.nonceLen` with a plain polynomial-time unary parameter function is plain +polynomial-time. -/ +@[program_certificate] +theorem computableInPolyTime_nonceLen_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} + {n : γ → ℕ} (hn : ComputableInPolyTime n encIn encUnary) : + ComputableInPolyTime (fun a => M.nonceLen (n a)) encIn encUnary := + M.nonceLen_polyTime.comp hn + +@[local fun_prop] +private theorem isPPTOn_keyGen_comp_tidy (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} + {n : γ → ℕ} (hn : ComputableTidilyInPolyTime n encIn encUnary) : + IsPPTOn encIn encBits (fun a => M.keyGen (n a)) := + M.keyGen_ppt.preprocess (ComputableInPolyTime.of_tidy hn) + +/-- Composing `M.keyGen` with a plain polynomial-time unary parameter function is strict PPT. -/ +@[program_certificate] +theorem isPPTOn_keyGen_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} + {n : γ → ℕ} (hn : ComputableInPolyTime n encIn encUnary) : + IsPPTOn encIn encBits (fun a => M.keyGen (n a)) := + M.keyGen_ppt.preprocess hn + +@[local fun_prop] +private theorem isPPTOn_sign_comp_tidy (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} + {sk msg nonce : γ → List Bool} + (hsk : ComputableTidilyInPolyTime sk encIn encBits) + (hmsg : ComputableTidilyInPolyTime msg encIn encBits) + (hnonce : ComputableTidilyInPolyTime nonce encIn encBits) : + IsPPTOn encIn encBits (fun a => M.sign (sk a) (msg a) (nonce a)) := + M.sign_ppt.preprocess (ComputableInPolyTime.of_tidy (hsk.prod (hmsg.prod hnonce))) + +/-- Composing `M.sign` with plain polynomial-time key, message, and nonce selectors is strict +PPT. -/ +@[program_certificate] +theorem isPPTOn_sign_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} + {sk msg nonce : γ → List Bool} + (hsk : ComputableInPolyTime sk encIn encBits) + (hmsg : ComputableInPolyTime msg encIn encBits) + (hnonce : ComputableInPolyTime nonce encIn encBits) : + IsPPTOn encIn encBits (fun a => M.sign (sk a) (msg a) (nonce a)) := + M.sign_ppt.preprocess (hsk.prod (hmsg.prod hnonce)) + +@[local fun_prop] +private theorem computableTidilyInPolyTime_verify_comp (M : NonceMACScheme) + {γ : Type} {encIn : γ ↪ List Bool} {sk msg nonce tag : γ → List Bool} + (hsk : ComputableTidilyInPolyTime sk encIn encBits) + (hmsg : ComputableTidilyInPolyTime msg encIn encBits) + (hnonce : ComputableTidilyInPolyTime nonce encIn encBits) + (htag : ComputableTidilyInPolyTime tag encIn encBits) : + ComputableTidilyInPolyTime + (fun a => M.verify (sk a) (msg a) (nonce a) (tag a)) encIn encBool := + M.verify_polyTime.tidy.comp (hsk.prod (hmsg.prod (hnonce.prod htag))) + +/-- Composing `M.verify` with plain polynomial-time key, message, nonce, and tag selectors is plain +polynomial-time. -/ +@[program_certificate] +theorem computableInPolyTime_verify_comp (M : NonceMACScheme) + {γ : Type} {encIn : γ ↪ List Bool} {sk msg nonce tag : γ → List Bool} + (hsk : ComputableInPolyTime sk encIn encBits) + (hmsg : ComputableInPolyTime msg encIn encBits) + (hnonce : ComputableInPolyTime nonce encIn encBits) + (htag : ComputableInPolyTime tag encIn encBits) : + ComputableInPolyTime + (fun a => M.verify (sk a) (msg a) (nonce a) (tag a)) encIn encBool := + M.verify_polyTime.comp (hsk.prod (hmsg.prod (hnonce.prod htag))) + +/-- Stateful nonce-based MAC tagging oracle that decodes `(msg, nonce)` from the framed query word +`request.2`, tags `(msg, nonce)` under `sk`, and prepends the returned `((msg, nonce), tag)` triple +to the transcript ([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]). -/ +noncomputable def signingPairOracle (M : NonceMACScheme) (sk : List Bool) + (request : Unit × List Bool) : + StateT (List ((List Bool × List Bool) × List Bool)) ProbComp (List Bool) := + fun queriedTriples => do + let msg := unframe request.2 + let nonce := dropFrame request.2 + let tag ← M.sign sk msg nonce + return (tag, ((msg, nonce), tag) :: queriedTriples) + +/-- The strong nonce-based MAC SUF-CMA experiment +([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]): sample `sk ← M.keyGen n`, run +the adaptive forger on `(n, [])` with oracle access to `M.signingPairOracle sk`, and accept when: +1. the candidate message has length `M.msgLen n` and the candidate nonce has length `M.nonceLen n`, +2. all nonces queried during the signing phase are pairwise distinct + (`decide (out.2.map (fun e => e.1.2)).Nodup`), +3. the candidate `((msg, nonce), tag)` triple was never returned by the tagging oracle + (`!out.2.contains out.1`), and +4. `M.verify sk msg nonce tag = true`. -/ +noncomputable def sufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (n : ℕ) : + ProbComp Bool := do + let sk ← M.keyGen n + let out ← (OracleComp.interpret + (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (M.signingPairOracle sk)) (adversary n [])).run [] + return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) && + decide (out.2.map (fun e => e.1.2)).Nodup && !out.2.contains out.1 && + M.verify sk out.1.1.1 out.1.1.2 out.1.2 + +/-- The fresh-message nonce-based MAC EUF-CMA experiment: identical to `sufCmaGame` except that the +candidate message `out.1.1.1` must never have been queried during the signing phase +(`!(out.2.map (fun e => e.1.1)).contains out.1.1.1`). -/ +noncomputable def eufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (n : ℕ) : + ProbComp Bool := do + let sk ← M.keyGen n + let out ← (OracleComp.interpret + (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (M.signingPairOracle sk)) (adversary n [])).run [] + return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) && + decide (out.2.map (fun e => e.1.2)).Nodup && + !(out.2.map (fun e => e.1.1)).contains out.1.1.1 && + M.verify sk out.1.1.1 out.1.1.2 out.1.2 + +/-- Running an oracle-PPT nonce-MAC forger against `signingPairOracle` is uniformly strict PPT in +the unary security parameter and secret key. -/ +@[program_certificate] +theorem isPPTOn_run_signingPairOracle (M : NonceMACScheme) {adversary : NonceMACForger} + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + IsPPTOn (encPair encUnary encBits) + (encPair (encPair (encPair encBits encBits) encBits) + (encList (encPair (encPair encBits encBits) encBits))) + (fun caller : ℕ × List Bool => + (OracleComp.interpret + (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (M.signingPairOracle caller.2)) (adversary caller.1 [])).run []) := by + obtain ⟨c, d, hlen⟩ := M.sign_ppt.length_le + have hhandler : IsPPTOn + (encPair (encPair encUnary encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + (encPair encBits (encList (encPair (encPair encBits encBits) encBits))) + (fun pair : (ℕ × List Bool) × + ((Unit × List Bool) × List ((List Bool × List Bool) × List Bool)) => + M.signingPairOracle pair.1.2 pair.2.1 pair.2.2) := by + unfold signingPairOracle + ppt + apply hadversary.run_interpret_preprocess + (prepare := fun caller : ℕ × List Bool => (caller.1, ([] : List Bool))) + (initial := fun _ => ([] : List ((List Bool × List Bool) × List Bool))) + (resources := fun caller query => + 2 * (c * (2 * caller.2.length + query.length + 3) ^ d) + 4 * query.length + 8) + (by fun_prop) hhandler (by fun_prop) + (fun _ _ => True) (fun _ => trivial) (by fun_prop) + intro caller request queriedTriples _ result hresult + simp only [signingPairOracle, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hresult + obtain ⟨tag, htag, rfl⟩ := hresult + have htagLen := hlen (caller.2, unframe request.2, dropFrame request.2) tag htag + simp only [encBits_apply, length_encPair] at htagLen + have hframe := length_unframe_add_dropFrame_le request.2 + have hbase : 2 * caller.2.length + 1 + + (2 * (unframe request.2).length + 1 + (dropFrame request.2).length) + 1 ≤ + 2 * caller.2.length + request.2.length + 3 := by omega + have hpow : c * (2 * caller.2.length + 1 + + (2 * (unframe request.2).length + 1 + (dropFrame request.2).length) + 1) ^ d ≤ + c * (2 * caller.2.length + request.2.length + 3) ^ d := + Nat.mul_le_mul_left c (Nat.pow_le_pow_left hbase d) + have htag_le : tag.length ≤ c * (2 * caller.2.length + request.2.length + 3) ^ d := + htagLen.trans hpow + refine ⟨trivial, by dsimp only; omega, ?_⟩ + simp only [encList_cons, List.length_append, length_frame, length_encPair, encBits_apply] + omega + +/-- Run the complete nonce-based MAC SUF-CMA experiment on its unary security parameter for any +oracle-PPT forger. -/ +@[program_certificate] +theorem isPPTOn_sufCmaGame (M : NonceMACScheme) {adversary : NonceMACForger} + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + IsPPTOn encUnary encBool (M.sufCmaGame adversary) := by + have hrun := M.isPPTOn_run_signingPairOracle hadversary + have hpost : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + (pair.2.1.1.1.length == M.msgLen pair.1.1) && + (pair.2.1.1.2.length == M.nonceLen pair.1.1) && + decide (pair.2.2.map (fun e => e.1.2)).Nodup && + !pair.2.2.contains pair.2.1 && + M.verify pair.1.2 pair.2.1.1.1 pair.2.1.1.2 pair.2.1.2) + (encPair (encPair encUnary encBits) + (encPair (encPair (encPair encBits encBits) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) encBool := by + polytime + exact M.keyGen_ppt.bind_with (hrun.bind_with hpost.isPPTOn) + +/-- The nonce-based MAC SUF-CMA experiment is uniformly strict PPT, independently of unused +auxiliary input. -/ +@[program_certificate] +theorem isPPT_sufCmaGame (M : NonceMACScheme) {adversary : NonceMACForger} + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + IsPPT encBool (fun n _ => M.sufCmaGame adversary n) := + ((M.isPPTOn_sufCmaGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT + +/-- Run the complete nonce-based MAC EUF-CMA experiment on its unary security parameter for any +oracle-PPT forger. -/ +@[program_certificate] +theorem isPPTOn_eufCmaGame (M : NonceMACScheme) {adversary : NonceMACForger} + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + IsPPTOn encUnary encBool (M.eufCmaGame adversary) := by + have hrun := M.isPPTOn_run_signingPairOracle hadversary + let EIn := encPair (encPair encUnary encBits) + (encPair (encPair (encPair encBits encBits) encBits) + (encList (encPair (encPair encBits encBits) encBits))) + have hmsgs : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + pair.2.2.map (fun e => e.1.1)) + EIn (encList encBits) := by + dsimp only [EIn]; fun_prop + have hmsg : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + pair.2.1.1.1) + EIn encBits := by + dsimp only [EIn]; fun_prop + have hcontains : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + (pair.2.2.map (fun e => e.1.1)).contains pair.2.1.1.1) + EIn encBool := + computableTidilyInPolyTime_contains hmsgs hmsg + have hprefix : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + (pair.2.1.1.1.length == M.msgLen pair.1.1) && + (pair.2.1.1.2.length == M.nonceLen pair.1.1) && + decide (pair.2.2.map (fun e => e.1.2)).Nodup) + EIn encBool := by + dsimp only [EIn]; polytime + have hver : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + M.verify pair.1.2 pair.2.1.1.1 pair.2.1.1.2 pair.2.1.2) + EIn encBool := by + dsimp only [EIn]; polytime + have hpost : ComputableTidilyInPolyTime + (fun pair : (ℕ × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + (pair.2.1.1.1.length == M.msgLen pair.1.1) && + (pair.2.1.1.2.length == M.nonceLen pair.1.1) && + decide (pair.2.2.map (fun e => e.1.2)).Nodup && + !(pair.2.2.map (fun e => e.1.1)).contains pair.2.1.1.1 && + M.verify pair.1.2 pair.2.1.1.1 pair.2.1.1.2 pair.2.1.2) + EIn encBool := + ComputableTidilyInPolyTime.bool_and.comp + ((ComputableTidilyInPolyTime.bool_and.comp + (hprefix.prod (ComputableTidilyInPolyTime.bool_not.comp hcontains))).prod hver) + exact M.keyGen_ppt.bind_with (hrun.bind_with hpost.isPPTOn) + +/-- The nonce-based MAC EUF-CMA experiment is uniformly strict PPT, independently of unused +auxiliary input. -/ +@[program_certificate] +theorem isPPT_eufCmaGame (M : NonceMACScheme) {adversary : NonceMACForger} + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + IsPPT encBool (fun n _ => M.eufCmaGame adversary n) := + ((M.isPPTOn_eufCmaGame hadversary).preprocess (ComputableInPolyTime.fst _ _)).isPPT + +/-- Strong existential unforgeability under nonce-respecting adaptive chosen-message attack +(`SUFCMA`) for a `NonceMACScheme` against uniform strict oracle-PPT adversaries +([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]). -/ +def SUFCMA (M : NonceMACScheme) : Prop := + Game.Indistinguishable + (fun adversary n => ProbComp.eval (M.sufCmaGame adversary n)) + (fun _ _ => PMF.pure false) + (IsOraclePPT (encPair (encPair encBits encBits) encBits)) + +/-- Strong nonce-based unforgeability gives negligible SUF-CMA forgery probability for every +oracle-PPT forger. -/ +theorem SUFCMA.negligible {M : NonceMACScheme} (h : M.SUFCMA) + (adversary : NonceMACForger) + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + Negligible (fun n => Game.succProbability (ProbComp.eval (M.sufCmaGame adversary n))) := by + simpa only [Game.advantage_pure_false] using h adversary hadversary + +/-- Establish nonce-based SUF-CMA security by bounding every oracle-PPT forger's success +probability. -/ +theorem SUFCMA.of_negligible {M : NonceMACScheme} + (h : ∀ adversary, IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary → + Negligible (fun n => Game.succProbability (ProbComp.eval (M.sufCmaGame adversary n)))) : + M.SUFCMA := by + intro adversary hadversary + simpa only [Game.advantage_pure_false] using h adversary hadversary + +/-- Fresh-message existential unforgeability under nonce-respecting adaptive chosen-message attack +(`EUFCMA`) for a `NonceMACScheme` against uniform strict oracle-PPT adversaries. -/ +def EUFCMA (M : NonceMACScheme) : Prop := + Game.Indistinguishable + (fun adversary n => ProbComp.eval (M.eufCmaGame adversary n)) + (fun _ _ => PMF.pure false) + (IsOraclePPT (encPair (encPair encBits encBits) encBits)) + +/-- Nonce-based EUF-CMA security gives negligible forgery probability for every oracle-PPT +forger. -/ +theorem EUFCMA.negligible {M : NonceMACScheme} (h : M.EUFCMA) + (adversary : NonceMACForger) + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + Negligible (fun n => Game.succProbability (ProbComp.eval (M.eufCmaGame adversary n))) := by + simpa only [Game.advantage_pure_false] using h adversary hadversary + +/-- Establish nonce-based EUF-CMA security by bounding every oracle-PPT forger's success +probability. -/ +theorem EUFCMA.of_negligible {M : NonceMACScheme} + (h : ∀ adversary, IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary → + Negligible (fun n => Game.succProbability (ProbComp.eval (M.eufCmaGame adversary n)))) : + M.EUFCMA := by + intro adversary hadversary + simpa only [Game.advantage_pure_false] using h adversary hadversary + +/-- **Quantitative EUF-CMA vs. SUF-CMA bound for `NonceMACScheme`**: for every `NonceMACScheme`, +adaptive forger, and security parameter `n`, the fresh-message `eufCmaGame` forgery probability is +at most the strong fresh-triple `sufCmaGame` forgery probability. -/ +theorem succProbability_eufCmaGame_le_sufCmaGame (M : NonceMACScheme) + (adversary : NonceMACForger) (n : ℕ) : + Game.succProbability (ProbComp.eval (M.eufCmaGame adversary n)) ≤ + Game.succProbability (ProbComp.eval (M.sufCmaGame adversary n)) := by + simp only [Game.succProbability, eufCmaGame, sufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure] + refine ENNReal.toNNReal_mono (PMF.apply_ne_top _ true) ?_ + rw [PMF.bind_apply, PMF.bind_apply] + refine ENNReal.tsum_le_tsum fun sk => ?_ + refine mul_le_mul_of_nonneg_left + (MACScheme.pmf_bind_pure_bool_le _ _ _ fun out _ hout => ?_) zero_le + simp only [Bool.and_eq_true, Bool.not_eq_true'] at hout ⊢ + refine ⟨⟨ hout.1.1, ?_ ⟩, hout.2⟩ + rw [Bool.eq_false_iff] + intro hmemTriple + have hmemMsg : out.1.1.1 ∈ out.2.map (fun e => e.1.1) := + List.mem_map_of_mem (f := fun e : (List Bool × List Bool) × List Bool => e.1.1) + (List.contains_iff_mem.mp hmemTriple) + have hcontainsMsg : (out.2.map (fun e => e.1.1)).contains out.1.1.1 = true := + List.contains_iff_mem.mpr hmemMsg + rw [hout.1.2] at hcontainsMsg + contradiction + +/-- Strong unforgeability (`SUFCMA`) implies fresh-message unforgeability (`EUFCMA`) for every +`NonceMACScheme`. -/ +theorem SUFCMA.eufCma {M : NonceMACScheme} (h : M.SUFCMA) : M.EUFCMA := by + apply EUFCMA.of_negligible + intro adversary hadversary + exact negligible_of_le (h.negligible adversary hadversary) + (M.succProbability_eufCmaGame_le_sufCmaGame adversary) + +private theorem mem_support_signingPairOracle (M : NonceMACScheme) (sk : List Bool) + (prog : WordOracleComp Unit ((List Bool × List Bool) × List Bool)) + (result : (List Bool × List Bool) × List Bool) + (queriedTriples : List ((List Bool × List Bool) × List Bool)) + (hmem : (result, queriedTriples) ∈ (ProbComp.eval ((OracleComp.interpret + (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (M.signingPairOracle sk)) prog).run [])).support) : + ∀ triple ∈ queriedTriples, + triple.2 ∈ (ProbComp.eval (M.sign sk triple.1.1 triple.1.2)).support := by + rw [ProbOracleComp.eval_run_interpret] at hmem + refine ProbOracleComp.run_interpret_invariant + (fun q s => ProbComp.eval (M.signingPairOracle sk q s)) + (fun s => ∀ triple ∈ s, + triple.2 ∈ (ProbComp.eval (M.sign sk triple.1.1 triple.1.2)).support) + ?_ prog [] (by simp) result queriedTriples hmem + intro ⟨⟨⟩, raw⟩ s hs a s' hstep triple htriple + simp only [signingPairOracle, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hstep + obtain ⟨tag, htag, htripleEq⟩ := hstep + cases htripleEq + rw [List.mem_cons] at htriple + rcases htriple with rfl | htail + · exact htag + · exact hs triple htail + +/-- For any `NonceMACScheme` whose valid tags on `M.msgLen n`-bit messages and `M.nonceLen n`-bit +nonces under supported secret keys agree with every tag in the support of `M.sign`, strong +triple-freshness (`!out.2.contains out.1`) in `sufCmaGame` is identical to `(msg, nonce)`-pair +freshness (`!(out.2.map Prod.fst).contains out.1.1`). -/ +theorem eval_sufCmaGame_eq_freshPair_of_unique_tag (M : NonceMACScheme) + (huniq : ∀ n sk, sk ∈ (ProbComp.eval (M.keyGen n)).support → + ∀ msg, msg.length = M.msgLen n → + ∀ nonce, nonce.length = M.nonceLen n → ∀ tag tag', + M.verify sk msg nonce tag = true → + tag' ∈ (ProbComp.eval (M.sign sk msg nonce)).support → tag' = tag) + (adversary : NonceMACForger) (n : ℕ) : + ProbComp.eval (M.sufCmaGame adversary n) = + ProbComp.eval (do + let sk ← M.keyGen n + let out ← (OracleComp.interpret + (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (M.signingPairOracle sk)) (adversary n [])).run [] + return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) && + decide (out.2.map (fun e => e.1.2)).Nodup && + !(out.2.map Prod.fst).contains out.1.1 && + M.verify sk out.1.1.1 out.1.1.2 out.1.2) := by + simp only [sufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure] + refine PMF.bind_congr_on_support _ _ _ fun sk hsk => ?_ + refine PMF.bind_congr_on_support _ _ _ fun ⟨⟨⟨msg, nonce⟩, tag⟩, queriedTriples⟩ hout => ?_ + have hinv := M.mem_support_signingPairOracle sk (adversary n []) + ((msg, nonce), tag) queriedTriples hout + congr 1 + by_cases hmsg : (msg.length == M.msgLen n) = true + · by_cases hnonce : (nonce.length == M.nonceLen n) = true + · by_cases hver : M.verify sk msg nonce tag = true + · have hmsgLen : msg.length = M.msgLen n := beq_iff_eq.mp hmsg + have hnonceLen : nonce.length = M.nonceLen n := beq_iff_eq.mp hnonce + have hmem_iff : ((msg, nonce), tag) ∈ queriedTriples ↔ + (msg, nonce) ∈ queriedTriples.map Prod.fst := by + rw [List.mem_map] + refine ⟨fun h => ⟨((msg, nonce), tag), h, rfl⟩, ?_⟩ + rintro ⟨⟨⟨qmsg, qnonce⟩, qtag⟩, hmemTriple, hpair_eq⟩ + cases hpair_eq + have hqtag := hinv ((msg, nonce), qtag) hmemTriple + have heq := huniq n sk hsk msg hmsgLen nonce hnonceLen tag qtag hver hqtag + subst heq + exact hmemTriple + simp only [hmsg, hnonce, hver, Bool.true_and, Bool.and_true, List.contains_eq_mem, + decide_eq_decide.mpr hmem_iff] + · simp [Bool.eq_false_iff.mpr hver] + · simp [Bool.eq_false_iff.mpr hnonce] + · simp [Bool.eq_false_iff.mpr hmsg] + +/-- For any `NonceMACScheme` whose valid `(nonce, tag)` pairs on `M.msgLen n`-bit messages under +supported secret keys agree with every `(nonce', tag')` produced on that message, `sufCmaGame` and +`eufCmaGame` have the exact same output distribution. -/ +theorem eval_sufCmaGame_eq_eufCmaGame_of_unique_tag (M : NonceMACScheme) + (huniq : ∀ n sk, sk ∈ (ProbComp.eval (M.keyGen n)).support → + ∀ msg, msg.length = M.msgLen n → + ∀ nonce, nonce.length = M.nonceLen n → ∀ nonce' tag tag', + M.verify sk msg nonce tag = true → + tag' ∈ (ProbComp.eval (M.sign sk msg nonce')).support → + nonce' = nonce ∧ tag' = tag) + (adversary : NonceMACForger) (n : ℕ) : + ProbComp.eval (M.sufCmaGame adversary n) = + ProbComp.eval (M.eufCmaGame adversary n) := by + simp only [sufCmaGame, eufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure] + refine PMF.bind_congr_on_support _ _ _ fun sk hsk => ?_ + refine PMF.bind_congr_on_support _ _ _ fun ⟨⟨⟨msg, nonce⟩, tag⟩, queriedTriples⟩ hout => ?_ + have hinv := M.mem_support_signingPairOracle sk (adversary n []) + ((msg, nonce), tag) queriedTriples hout + congr 1 + by_cases hmsg : (msg.length == M.msgLen n) = true + · by_cases hnonce : (nonce.length == M.nonceLen n) = true + · by_cases hver : M.verify sk msg nonce tag = true + · have hmsgLen : msg.length = M.msgLen n := beq_iff_eq.mp hmsg + have hnonceLen : nonce.length = M.nonceLen n := beq_iff_eq.mp hnonce + have hmem_iff : ((msg, nonce), tag) ∈ queriedTriples ↔ + msg ∈ queriedTriples.map (fun e => e.1.1) := by + rw [List.mem_map] + refine ⟨fun h => ⟨((msg, nonce), tag), h, rfl⟩, ?_⟩ + rintro ⟨⟨⟨qmsg, qnonce⟩, qtag⟩, hmemTriple, hmsg_eq⟩ + dsimp only at hmsg_eq + subst qmsg + have hqtag := hinv ((msg, qnonce), qtag) hmemTriple + obtain ⟨rfl, rfl⟩ := huniq n sk hsk msg hmsgLen nonce hnonceLen qnonce tag qtag hver hqtag + exact hmemTriple + simp only [hmsg, hnonce, hver, Bool.true_and, Bool.and_true, List.contains_eq_mem, + decide_eq_decide.mpr hmem_iff] + · simp [Bool.eq_false_iff.mpr hver] + · simp [Bool.eq_false_iff.mpr hnonce] + · simp [Bool.eq_false_iff.mpr hmsg] + +/-- Under the unique-`(nonce, tag)` hypothesis of `eval_sufCmaGame_eq_eufCmaGame_of_unique_tag`, +strong unforgeability (`SUFCMA`) is equivalent to fresh-message unforgeability (`EUFCMA`). -/ +theorem sufCma_iff_eufCma_of_unique_tag (M : NonceMACScheme) + (huniq : ∀ n sk, sk ∈ (ProbComp.eval (M.keyGen n)).support → + ∀ msg, msg.length = M.msgLen n → + ∀ nonce, nonce.length = M.nonceLen n → ∀ nonce' tag tag', + M.verify sk msg nonce tag = true → + tag' ∈ (ProbComp.eval (M.sign sk msg nonce')).support → + nonce' = nonce ∧ tag' = tag) : + M.SUFCMA ↔ M.EUFCMA := by + refine ⟨SUFCMA.eufCma, fun h => ?_⟩ + apply SUFCMA.of_negligible + intro adversary hadversary + refine (h.negligible adversary hadversary).congr fun n => ?_ + rw [M.eval_sufCmaGame_eq_eufCmaGame_of_unique_tag huniq adversary n] + +end NonceMACScheme + +/-- Alias for `NonceMACScheme.SUFCMA`. -/ +abbrev NonceSUFCMA := NonceMACScheme.SUFCMA + +/-- Alias for `NonceMACScheme.EUFCMA`. -/ +abbrev NonceEUFCMA := NonceMACScheme.EUFCMA + end Cslib.Crypto diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index c3864420a1..686ff625dd 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -7,13 +7,17 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Computability.Probabilistic.LinearHash +public import Complexity.Crypto.Computational.MAC public import Complexity.Crypto.Computational.PseudorandomFunction +public import Complexity.Foundations.Data.BitString.List.Operations public import Complexity.Languages.Probabilistic.Simulation public import Complexity.Probability.BitString.LinearHash public import Complexity.Probability.BitString.SubsetSum public import Complexity.Probability.HashFamily public import Complexity.Probability.HashFamily.Polynomial public import Complexity.Probability.PairwiseIndependentHash.Universal +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Length import Complexity.Computability.Probabilistic.Oracle.Composition import Complexity.Crypto.Negligible.Basic @@ -113,15 +117,20 @@ This module formalizes: `maskedNonceStrongGame`, `maskedNonceGame`, `nonceFnDistinguisher`, `prfFnDist`, `prfNonceStrongGame`, `prfNonceGame`, `prfNonceStrongGame_le_of_distinguisher`, `prfNonceGame_le_of_distinguisher`, `PseudorandomFunction.negligible_prfNonceStrongGame`, - `PseudorandomFunction.negligible_prfNonceGame`)**: models Boneh–Shoup Attack Game 7.4 and - Theorem 7.10 ([BonehShoup2023], Section 7.5.1, p. 274) under a statistical `IsDeltaUniversalHash` - family, where the adversary adaptively chooses distinct signing nonces `x_i : N` and outputs a - candidate forgery `((m', x'), t')` at any (issued or unissued) nonce `x'`, achieving forgery - probability at most `max ε (1 / |Y|) ≤ ε + 1 / |Y|` under a random function - `rf ← PMF.uniformOfFintype (N → Y)`, and at most `ε.toReal + (2 ^ n)⁻¹ + Game.advantage ...` - under a PRF pad family `prfFnDist family n` when given an `OracleDistinguisher` `D` simulating - `nonceFnDistinguisher` (constructing `D` from a word-level `IsOraclePPT` nonce-MAC forger remains - open in #736). + `PseudorandomFunction.negligible_prfNonceGame`, `carterWegmanNonceMAC`, `cwNonceLogHandler`, + `prfNonceToPrfDistinguisher`, `isOraclePPT_prfNonceToPrfDistinguisher`, + `eval_prfRealGame_prfNonceToPrfDistinguisher`, + `eval_prfIdealGame_prfNonceToPrfDistinguisher_le`, `sufCmaGame_carterWegmanNonceMAC_toReal_le`, + `PseudorandomFunction.sufCma_carterWegmanNonceMAC`, + `PseudorandomFunction.eufCma_carterWegmanNonceMAC`)**: models Boneh–Shoup Attack Game 7.4 and + Theorem 7.10 ([BonehShoup2023], Section 7.5.1, p. 274) both information-theoretically and + computationally (`NonceMACScheme`), where the adversary adaptively chooses distinct signing + nonces `x_i : N` and outputs a candidate forgery `((m', x'), t')` at any (issued or unissued) + nonce `x'`, achieving forgery probability at most `max ε (1 / |Y|) ≤ ε + 1 / |Y|` under a random + function `rf ← PMF.uniformOfFintype (N → Y)`, at most `ε.toReal + (2 ^ n)⁻¹ + Game.advantage ...` + under a PRF pad family `prfFnDist family n` via the `IsOraclePPT encBool` reduction wrapper + `prfNonceToPrfDistinguisher`, and asymptotic `NonceMACScheme.SUFCMA` and `NonceMACScheme.EUFCMA` + security under `PseudorandomFunction family` and `Negligible ε`. 8. **Randomized Carter–Wegman MAC (`RandomNonceForger`, `randomNonceFnHandler`, `randomNonceSimHandler`, `checkRandomNonceSUF`, `checkRandomNonceEUF`, `randomNonceStrongGame`, `randomNonceGame`, `randomNonceStrongGame_le`, `randomNonceGame_le`, @@ -129,18 +138,27 @@ This module formalizes: `prfRandomNonceStrongGame`, `prfRandomNonceGame`, `prfRandomNonceStrongGame_le_of_distinguisher`, `prfRandomNonceGame_le_of_distinguisher`, `PseudorandomFunction.negligible_prfRandomNonceStrongGame`, - `PseudorandomFunction.negligible_prfRandomNonceGame`)**: models Boneh–Shoup Section 7.4, - Theorem 7.9 ([BonehShoup2023], pp. 267–270) under a statistical `IsDeltaUniversalHash` family, - where the signer samples a fresh uniform nonce `x_i ← PMF.uniformOfFintype N` on each signing - query, bounding any `Q`-query adaptive forger's winning probability by + `PseudorandomFunction.negligible_prfRandomNonceGame`, `carterWegmanRandomMAC`, + `cwRandomNonceLogHandler`, `prfRandomNonceToPrfDistinguisher`, + `isOraclePPT_prfRandomNonceToPrfDistinguisher`, + `eval_prfRealGame_prfRandomNonceToPrfDistinguisher`, + `eval_prfIdealGame_prfRandomNonceToPrfDistinguisher_le`, + `sufCmaGame_carterWegmanRandomMAC_toReal_le`, + `PseudorandomFunction.sufCma_carterWegmanRandomMAC`, + `PseudorandomFunction.eufCma_carterWegmanRandomMAC`, + `PseudorandomFunction.oneTimeEUFCMA_carterWegmanRandomMAC`)**: models Boneh–Shoup Section 7.4, + Theorem 7.9 ([BonehShoup2023], pp. 267–270) both information-theoretically and computationally + (`MACScheme`), where the signer samples a fresh uniform nonce `x_i ← PMF.uniformOfFintype N` on + each signing query, bounding any `Q`-query adaptive forger's winning probability by `((∑ i ∈ Finset.range Q, i : ℕ) : ℝ≥0∞) / |N| + max ε (1 / |Y|) ≤` `Q ^ 2 / (2 * |N|) + 1 / |Y| + ε` - under a random function and adding the PRF distinguishing advantage under `prfFnDist family n` - when given an `OracleDistinguisher` `D` simulating `randomNonceFnDistinguisher` (constructing `D` - from a word-level `IsOraclePPT` forger and packaging randomized Carter–Wegman as a `MACScheme` - with `SUFCMA` remain open in #736). + under a random function, adding the PRF distinguishing advantage of the `IsOraclePPT encBool` + reduction wrapper `prfRandomNonceToPrfDistinguisher` under `prfFnDist family n`, and proving + asymptotic `MACScheme.SUFCMA`, `MACScheme.EUFCMA`, and `MACScheme.OneTimeEUFCMA` security under + `PseudorandomFunction family` and `Negligible ε`. 9. **Concrete instantiations** for Carter–Wegman polynomial hashing (`xpolyHash`, bound - `(ℓ + 1) / |F|`), Boolean-matrix linear hashing (`BitString.LinearHash.hash`, bound `2⁻ᵐ`), + `(ℓ + 1) / |F|`), Boolean-matrix linear hashing (`BitString.LinearHash.hash` and computational + `linearHashNonceMAC` / `linearHashRandomMAC` via `BitString.LinearHash.wordHash`, bound `2⁻ᵐ`), subset-sum hashing (`BitString.SubsetSum.hash`, bound `1 / |G|`), and pairwise independent hash families (`IsPairwiseIndependentHash`, bound `1 / |Y|`). @@ -192,7 +210,12 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.nonceFnDistinguisher`, `Cslib.Crypto.Protocols.CarterWegman.prfFnDist`, `Cslib.Crypto.Protocols.CarterWegman.prfNonceStrongGame`, - `Cslib.Crypto.Protocols.CarterWegman.prfNonceGame`: full nonce-based Carter–Wegman experiments + `Cslib.Crypto.Protocols.CarterWegman.prfNonceGame`, + `Cslib.Crypto.Protocols.CarterWegman.carterWegmanNonceMAC`, + `Cslib.Crypto.Protocols.CarterWegman.cwNonceLogHandler`, + `Cslib.Crypto.Protocols.CarterWegman.prfNonceToPrfDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.linearHashNonceMAC`: full nonce-based Carter–Wegman + experiments, `NonceMACScheme` packaging, and `OracleDistinguisher` reduction wrapper (Boneh–Shoup Attack Game 7.4 and Theorem 7.10). * `Cslib.Crypto.Protocols.CarterWegman.RandomNonceForger`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceFnHandler`, @@ -205,7 +228,12 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.maskedRandomNonceGame`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceFnDistinguisher`, `Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceStrongGame`, - `Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceGame`: randomized Carter–Wegman experiments + `Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceGame`, + `Cslib.Crypto.Protocols.CarterWegman.carterWegmanRandomMAC`, + `Cslib.Crypto.Protocols.CarterWegman.cwRandomNonceLogHandler`, + `Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceToPrfDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.linearHashRandomMAC`: randomized Carter–Wegman experiments, + `MACScheme` packaging, and `OracleDistinguisher` reduction wrapper (Boneh–Shoup Section 7.4, Theorem 7.9, p. 270). ## Main results @@ -253,6 +281,7 @@ This module formalizes: PRF-masked Carter–Wegman security, `IsOraclePPT` admissibility, and asymptotic security (after Boneh–Shoup Section 7.5, Theorem 7.10). * `Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_nonceFnHandler`, + `Cslib.Crypto.Protocols.CarterWegman.probOracleComp_uniform_bind_run_interpret_nonceFnHandler`, `Cslib.Crypto.Protocols.CarterWegman.seed_uniform_checkNonceSUF_le`, `Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_le_max`, `Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_le`, @@ -262,10 +291,19 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.prfNonceStrongGame_le_of_distinguisher`, `Cslib.Crypto.Protocols.CarterWegman.prfNonceGame_le_of_distinguisher`, `Cslib.Crypto.PseudorandomFunction.negligible_prfNonceStrongGame`, - `Cslib.Crypto.PseudorandomFunction.negligible_prfNonceGame`: full nonce-based Carter–Wegman + `Cslib.Crypto.PseudorandomFunction.negligible_prfNonceGame`, + `Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfNonceToPrfDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfNonceToPrfDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfNonceToPrfDistinguisher_le`, + `Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_carterWegmanNonceMAC_toReal_le`, + `Cslib.Crypto.PseudorandomFunction.sufCma_carterWegmanNonceMAC`, + `Cslib.Crypto.PseudorandomFunction.eufCma_carterWegmanNonceMAC`: full nonce-based Carter–Wegman security (Boneh–Shoup Attack Game 7.4 and Theorem 7.10). * `Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_randomNonceFnHandler`, + `probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceSimHandler_not_nodup_le`, + `Cslib.Crypto.Protocols.CarterWegman.probOracleComp_randomNonceSimHandler_not_nodup_le`, + `Cslib.Crypto.Protocols.CarterWegman.seed_uniform_probOracleComp_checkRandomNonceSUF_le`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_le_sum_add_max`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_le`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceGame_le`, @@ -273,7 +311,14 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceStrongGame_le_of_distinguisher`, `Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceGame_le_of_distinguisher`, `Cslib.Crypto.PseudorandomFunction.negligible_prfRandomNonceStrongGame`, - `Cslib.Crypto.PseudorandomFunction.negligible_prfRandomNonceGame`: randomized Carter–Wegman + `Cslib.Crypto.PseudorandomFunction.negligible_prfRandomNonceGame`, + `Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfRandomNonceToPrfDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfRandomNonceToPrfDistinguisher`, + `Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfRandomNonceToPrfDistinguisher_le`, + `Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_carterWegmanRandomMAC_toReal_le`, + `Cslib.Crypto.PseudorandomFunction.sufCma_carterWegmanRandomMAC`, + `Cslib.Crypto.PseudorandomFunction.eufCma_carterWegmanRandomMAC`, + `Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_carterWegmanRandomMAC`: randomized Carter–Wegman security (Boneh–Shoup Section 7.4, Theorem 7.9, p. 270). * `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_xpolyHash_le`, `Cslib.Crypto.Protocols.CarterWegman.counterGame_xpolyHash_le`, @@ -284,6 +329,14 @@ This module formalizes: `Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_linearHash_le`, `Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_linearHash_le`, `Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_linearHash_le`, + `Cslib.Crypto.Protocols.CarterWegman.isDeltaUniversalHash_linearHashWordHash`, + `Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_linearHashNonceMAC_toReal_le`, + `Cslib.Crypto.PseudorandomFunction.sufCma_linearHashNonceMAC`, + `Cslib.Crypto.PseudorandomFunction.eufCma_linearHashNonceMAC`, + `Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_linearHashRandomMAC_toReal_le`, + `Cslib.Crypto.PseudorandomFunction.sufCma_linearHashRandomMAC`, + `Cslib.Crypto.PseudorandomFunction.eufCma_linearHashRandomMAC`, + `Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_linearHashRandomMAC`, `Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_subsetSum_le`, `Cslib.Crypto.Protocols.CarterWegman.counterGame_subsetSum_le`, `Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_subsetSum_le`, @@ -2047,7 +2100,7 @@ private theorem not_nodup_map_append_of_mem {tr : List ((M × N) × Y)} (m : M) omit [AddGroup Y] in private theorem run_interpret_bind_of_not_nodup {ι : Type} {spec : OracleSpec ι} {α β : Type} (oracle : (q : ι) → StateT (List ((M × N) × Y)) PMF (spec q)) - (happ : ∀ q tr res, res ∈ (oracle q tr).support → ∃ e, res.2 = tr ++ [e]) + (happ : ∀ q tr res, res ∈ (oracle q tr).support → ∃ s, res.2 = tr ++ s) (prog : OracleComp spec α) {tr : List ((M × N) × Y)} (hnot : ¬ (tr.map (fun e => e.1.2)).Nodup) (g : α → List ((M × N) × Y) → PMF β) (c : PMF β) @@ -2063,7 +2116,7 @@ private theorem run_interpret_bind_of_not_nodup {ι : Type} {spec : OracleSpec ((OracleComp.interpret oracle (cont res.1)).run res.2).bind (fun res' => g res'.1 res'.2) = c := by intro res hres - obtain ⟨e, he⟩ := happ q tr res hres + obtain ⟨s, he⟩ := happ q tr res hres refine ih res.1 (he ▸ ?_) rw [List.map_append] exact fun h => hnot (h.sublist (List.sublist_append_left _ _)) @@ -2089,18 +2142,19 @@ theorem uniform_bind_run_interpret_nonceFnHandler {α β : Type} [Fintype N] [De (PMF.uniformOfFintype (N → Y)).bind fun table => post res.1 res.2 (reconstructPadFn hash k res.2 table)) := by have happ_fn (padFn : N → Y) : - ∀ q tr₁ res, res ∈ (nonceFnHandler hash k padFn q tr₁).support → ∃ e, res.2 = tr₁ ++ [e] := by + ∀ q tr₁ res, res ∈ (nonceFnHandler hash k padFn q tr₁).support → + ∃ s, res.2 = tr₁ ++ s := by intro q tr₁ res hres simp only [nonceFnHandler, PMF.support_pure, Set.mem_singleton_iff] at hres - exact ⟨(q, _), congrArg Prod.snd hres⟩ + exact ⟨[(q, _)], congrArg Prod.snd hres⟩ have happ_sim : ∀ q tr₁ res, res ∈ (nonceSimHandler (M := M) (N := N) (Y := Y) q tr₁).support → - ∃ e, res.2 = tr₁ ++ [e] := by + ∃ s, res.2 = tr₁ ++ s := by intro q tr₁ res hres simp only [nonceSimHandler, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, Set.mem_singleton_iff] at hres rcases hres with ⟨t, -, hres⟩ - exact ⟨(q, t), congrArg Prod.snd hres⟩ + exact ⟨[(q, t)], congrArg Prod.snd hres⟩ have hpost_sim : ∀ a tr', ¬ (tr'.map (fun e => e.1.2)).Nodup → ((PMF.uniformOfFintype (N → Y)).bind fun table => post a tr' (reconstructPadFn hash k tr' table)) = c := by @@ -2151,6 +2205,124 @@ theorem uniform_bind_run_interpret_nonceFnHandler {α β : Type} [Fintype N] [De run_interpret_bind_of_not_nodup _ happ_sim _ hnodup _ c hpost_sim simp only [hlhs, hrhs, PMF.bind_const] +/-- **Multi-query simulation equivalence for `nonceFnHandler` on `ProbOracleComp`**: +lifting `uniform_bind_run_interpret_nonceFnHandler` to programs with private coin flips +(`ProbOracleComp (fun _ : M × N => Y) α`). -/ +theorem probOracleComp_uniform_bind_run_interpret_nonceFnHandler {α β : Type} + [Fintype N] [DecidableEq N] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) + (prog : ProbOracleComp (fun _ : M × N => Y) α) (tr : List ((M × N) × Y)) + (post : α → List ((M × N) × Y) → (N → Y) → PMF β) (c : PMF β) + (hpost : ∀ a tr' padFn, ¬ (tr'.map (fun e => e.1.2)).Nodup → post a tr' padFn = c) : + ((PMF.uniformOfFintype (N → Y)).bind fun table => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hash k (reconstructPadFn hash k tr table))) prog).run tr).bind + fun res => post res.1 res.2 (reconstructPadFn hash k tr table)) = + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + nonceSimHandler) prog).run tr).bind fun res => + (PMF.uniformOfFintype (N → Y)).bind fun table => + post res.1 res.2 (reconstructPadFn hash k res.2 table)) := by + have happ_fn (padFn : N → Y) : + ∀ q tr₁ res, res ∈ (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hash k padFn) q tr₁).support → ∃ s, res.2 = tr₁ ++ s := by + intro q tr₁ res hres + cases q with + | inl m => + simp only [ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨i, -, hres⟩ + exact ⟨[], by simp [congrArg Prod.snd hres]⟩ + | inr q => + simp only [ProbOracleComp.handler, nonceFnHandler, PMF.support_pure, + Set.mem_singleton_iff] at hres + exact ⟨[(q, _)], congrArg Prod.snd hres⟩ + have happ_sim : + ∀ q tr₁ res, res ∈ (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceSimHandler (M := M) (N := N) (Y := Y)) q tr₁).support → + ∃ s, res.2 = tr₁ ++ s := by + intro q tr₁ res hres + cases q with + | inl m => + simp only [ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨i, -, hres⟩ + exact ⟨[], by simp [congrArg Prod.snd hres]⟩ + | inr q => + simp only [ProbOracleComp.handler, nonceSimHandler, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨t, -, hres⟩ + exact ⟨[(q, t)], congrArg Prod.snd hres⟩ + have hpost_sim : ∀ a tr', ¬ (tr'.map (fun e => e.1.2)).Nodup → + ((PMF.uniformOfFintype (N → Y)).bind fun table => + post a tr' (reconstructPadFn hash k tr' table)) = c := by + intro a tr' hnot + simp only [hpost a tr' _ hnot, PMF.bind_const] + induction prog using OracleComp.induction generalizing tr with + | pure a => + simp [PMF.monad_pure_eq_pure] + | query_bind q cont ih => + by_cases hnodup : (tr.map (fun e => e.1.2)).Nodup + · cases q with + | inl m => + simp only [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_comm (PMF.uniformOfFintype (N → Y)) (ProbComp.unifOracle m)] + congr 1; funext i + exact ih i tr + | inr q => + simp only [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + ProbOracleComp.handler, nonceFnHandler, nonceSimHandler, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + by_cases hx : q.2 ∈ tr.map (fun e => e.1.2) + · have hnot (t : Y) : ¬ ((tr ++ [(q, t)]).map (fun e => e.1.2)).Nodup := + not_nodup_map_append_of_mem q.1 t hx + have hlhs (table : N → Y) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hash k (reconstructPadFn hash k tr table))) + (cont (sign hash k (reconstructPadFn hash k tr table q.2) q.1))).run + (tr ++ [(q, sign hash k (reconstructPadFn hash k tr table q.2) q.1)])).bind + (fun res => post res.1 res.2 (reconstructPadFn hash k tr table)) = c := + run_interpret_bind_of_not_nodup _ (happ_fn _) _ (hnot _) _ c + (fun a tr' h => hpost a tr' _ h) + have hrhs (t : Y) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + nonceSimHandler) (cont t)).run (tr ++ [(q, t)])).bind + (fun res => (PMF.uniformOfFintype (N → Y)).bind fun table => + post res.1 res.2 (reconstructPadFn hash k res.2 table)) = c := + run_interpret_bind_of_not_nodup _ happ_sim _ (hnot t) _ c hpost_sim + simp only [hlhs, hrhs, PMF.bind_const] + · rw [uniform_reconstructPadFn_step hash k q.1 hx + (fun t tr' fn => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hash k fn)) (cont t)).run tr').bind + fun res => post res.1 res.2 fn)] + congr 1; funext t + exact ih t (tr ++ [(q, t)]) + · have hlhs (table : N → Y) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hash k (reconstructPadFn hash k tr table))) + (OracleComp.query q >>= cont)).run tr).bind + (fun res => post res.1 res.2 (reconstructPadFn hash k tr table)) = c := + run_interpret_bind_of_not_nodup _ (happ_fn _) _ hnodup _ c + (fun a tr' h => hpost a tr' _ h) + have hrhs : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + nonceSimHandler) (OracleComp.query q >>= cont)).run tr).bind + (fun res => (PMF.uniformOfFintype (N → Y)).bind fun table => + post res.1 res.2 (reconstructPadFn hash k res.2 table)) = c := + run_interpret_bind_of_not_nodup _ happ_sim _ hnodup _ c hpost_sim + simp only [hlhs, hrhs, PMF.bind_const] + variable [DecidableEq M] [DecidableEq N] [DecidableEq Y] /-- Nonce-based SUF-CMA verification predicate on a query–tag transcript `tr` and pad function @@ -2559,6 +2731,818 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfNonceGame exact ENNReal.toNNReal_mono (PMF.apply_ne_top _ _) (maskedNonceGame_le_maskedNonceStrongGame (seed n) (prfFnDist family n) (hash n) (forger n)) +private theorem interpret_deterministic_run_interpret {State α : Type} + (g : List Bool → List Bool) + (handler : Unit × List Bool → StateT State (WordOracleComp Unit) (List Bool)) + (prog : WordOracleComp Unit α) (s : State) : + OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin (fun request => pure (g request.2))) + ((OracleComp.interpret + (ProbOracleComp.handler + (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) + handler) + prog).run s) = + (OracleComp.interpret + (ProbOracleComp.handler + (fun k => StateT.lift (ProbComp.unifFin k)) + (fun request state => + OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin (fun req => pure (g req.2))) + (handler request state))) + prog).run s := by + have hf : IsMonadHom (WordOracleComp Unit) ProbComp + (OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin (fun request => pure (g request.2)))) := + PFunctor.FreeM.isMonadHom_liftM _ + rw [OracleComp.map_run_interpret hf] + congr 2 + funext q state + cases q with + | inl k => simp [ProbOracleComp.handler, StateT.lift, ProbComp.unifFin] + | inr request => rfl + +@[simp] +private theorem interpret_unifFin {α : Type} (p : ProbComp α) : + OracleComp.interpret ProbComp.unifFin p = p := + OracleComp.interpret_query_eq_self p + +/-- **Computational nonce-based Carter–Wegman MAC (`NonceMACScheme`)** +([BonehShoup2023], Section 7.5, Figure 7.3 and Theorem 7.10, p. 274): +given a polynomial-time message-length schedule `msgLen : ℕ → ℕ`, a strict-PPT hash-key sampler +`seed : ℕ → ProbComp (List Bool)`, a polynomial-time hash evaluator +`hash : ℕ → List Bool → List Bool → List Bool`, and a polynomial-time PRF family +`family : List Bool → List Bool → List Bool`: +* `keyGen n` samples `k ← seed n` and `prfKey ← BitString.sampleList n`, returning the framed pair + `encPair encBits encBits (k, prfKey)`. +* `sign sk msg nonce` recovers `k := unframe sk`, `prfKey := dropFrame sk`, and + `n := prfKey.length`; if `msg.length == msgLen n` and `nonce.length == n`, it returns the `n`-bit + Carter–Wegman tag `BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n]`, + and otherwise `[]`. +* `verify sk msg nonce tag` checks `msg.length == msgLen n`, `nonce.length == n`, and + `BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n] == tag`. -/ +noncomputable def carterWegmanNonceMAC (msgLen : ℕ → ℕ) + (seed : ℕ → ProbComp (List Bool)) + (hash : ℕ → List Bool → List Bool → List Bool) + (family : List Bool → List Bool → List Bool) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) : NonceMACScheme where + msgLen := msgLen + nonceLen n := n + msgLen_polyTime := hmsgLen + nonceLen_polyTime := by polytime + keyGen n := do + let k ← seed n + let prfKey ← BitString.sampleList n + return encPair encBits encBits (k, prfKey) + sign sk msg nonce := + let k := unframe sk + let prfKey := dropFrame sk + let n := prfKey.length + if (msg.length == msgLen n) && (nonce.length == n) then + pure (BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n]) + else + pure [] + verify sk msg nonce tag := + let k := unframe sk + let prfKey := dropFrame sk + let n := prfKey.length + (msg.length == msgLen n) && (nonce.length == n) && + (BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n] == tag) + keyGen_ppt := by ppt + sign_ppt := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hfamily_tidy := hfamily.tidy + have hprf : ComputableTidilyInPolyTime + (fun p : List Bool × List Bool × List Bool => + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2) + (encPair encBits (encPair encBits encBits)) encBits := by + have heq : (fun p : List Bool × List Bool × List Bool => + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2) = + (fun p : List Bool × List Bool × List Bool => + if p.2.2.length == (dropFrame p.1).length then + family (dropFrame p.1) p.2.2 + else + []) := by + funext p + simp [prfOracle] + rw [heq] + polytime + have hbody : ComputableTidilyInPolyTime + (fun p : List Bool × List Bool × List Bool => + let k := unframe p.1 + let prfKey := dropFrame p.1 + let n := prfKey.length + if (p.2.1.length == msgLen n) && (p.2.2.length == n) then + BitString.listXor n [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n] + else + []) + (encPair encBits (encPair encBits encBits)) encBits := by + polytime + have hpure : (fun p : List Bool × List Bool × List Bool => + let k := unframe p.1 + let prfKey := dropFrame p.1 + let n := prfKey.length + if (p.2.1.length == msgLen n) && (p.2.2.length == n) then + (pure (BitString.listXor n + [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n]) : ProbComp (List Bool)) + else + pure []) = + (fun p : List Bool × List Bool × List Bool => + pure ( + let k := unframe p.1 + let prfKey := dropFrame p.1 + let n := prfKey.length + if (p.2.1.length == msgLen n) && (p.2.2.length == n) then + BitString.listXor n [hash n k p.2.1, (prfOracle family n prfKey p.2.2).take n] + else + [])) := by + funext p + dsimp only + split <;> rfl + rw [hpure] + exact hbody.isPPTOn + verify_polyTime := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hfamily_tidy := hfamily.tidy + have hprf : ComputableTidilyInPolyTime + (fun p : List Bool × List Bool × List Bool × List Bool => + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2.1) + (encPair encBits (encPair encBits (encPair encBits encBits))) encBits := by + have heq : (fun p : List Bool × List Bool × List Bool × List Bool => + prfOracle family (dropFrame p.1).length (dropFrame p.1) p.2.2.1) = + (fun p : List Bool × List Bool × List Bool × List Bool => + if p.2.2.1.length == (dropFrame p.1).length then + family (dropFrame p.1) p.2.2.1 + else + []) := by + funext p + simp [prfOracle] + rw [heq] + polytime + exact .of_tidy (by polytime) + verify_sign := by + intro n sk hsk msg hmsg nonce hnonce tag htag + simp only [ProbComp.eval_bind, ProbComp.eval_pure, BitString.eval_sampleList, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hsk + rcases hsk with ⟨k, -, prfKey, hprfKey, rfl⟩ + have hprfLen : prfKey.length = n := BitString.length_of_mem_support_uniformList hprfKey + simp only [encPair_apply, encBits_apply, dropFrame_frame_append, + hprfLen, hmsg, hnonce, beq_self_eq_true, Bool.and_self, ↓reduceIte, + ProbComp.eval_pure, PMF.mem_support_pure_iff] at htag ⊢ + subst htag + simp + +/-- Open stateful handler for the nonce-based Carter–Wegman PRF reduction +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274): given the hash key `k` and a framed +signing request `request.2`, it decodes `msg := unframe request.2` and +`nonce := dropFrame request.2`. When `msg.length == msgLen n` and `nonce.length == n`, it queries +the external oracle on `((), nonce)` (reading `n` bits `pad`), computes +`tag := BitString.listXor n [hash n k msg, pad]`, and prepends `((msg, nonce), tag)` to +`queriedTriples`; otherwise it returns `[]` and prepends `((msg, nonce), [])` without querying the +external oracle. -/ +def cwNonceLogHandler (msgLen : ℕ → ℕ) (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (request : Unit × List Bool) : + StateT (List ((List Bool × List Bool) × List Bool)) (WordOracleComp Unit) (List Bool) := + fun queriedTriples => + let msg := unframe request.2 + let nonce := dropFrame request.2 + if (msg.length == msgLen n) && (nonce.length == n) then + (fun pad => + let tag := BitString.listXor n [hash n k msg, pad] + (tag, ((msg, nonce), tag) :: queriedTriples)) <$> + (List.take n <$> ProbOracleComp.query ((), nonce)) + else + pure ([], ((msg, nonce), []) :: queriedTriples) + +/-- Oracle reduction turning an adaptive word-level `NonceMACForger` into an `OracleDistinguisher` +for the PRF security game ([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274): +1. Sample `k ← seed n`. +2. Run `adversary n []`, answering each signing query via `cwNonceLogHandler msgLen hash n k`. +3. Query the external oracle on the candidate nonce `out.1.1.2` (reading `n` bits `pad`), and + accept iff `msg.length == msgLen n`, `nonce.length == n`, all queried nonces were pairwise + distinct, the candidate `((msg, nonce), tag)` triple was not returned by the signing oracle, and + `BitString.listXor n [hash n k msg, pad] == tag`. -/ +def prfNonceToPrfDistinguisher (msgLen : ℕ → ℕ) (seed : ℕ → ProbComp (List Bool)) + (hash : ℕ → List Bool → List Bool → List Bool) (adversary : NonceMACForger) : + OracleDistinguisher := fun n _ => do + let k ← ProbOracleComp.sample (seed n) + let out ← + (OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (cwNonceLogHandler msgLen hash n k)) + (adversary n [])).run [] + (fun pad => (out.1.1.1.length == msgLen n) && (out.1.1.2.length == n) && + decide (out.2.map (fun e => e.1.2)).Nodup && !out.2.contains out.1 && + (BitString.listXor n [hash n k out.1.1.1, pad] == out.1.2)) <$> + (List.take n <$> ProbOracleComp.query ((), out.1.1.2)) + +/-- `prfNonceToPrfDistinguisher` is uniformly strict oracle-PPT (`IsOraclePPT encBool`) whenever +`msgLen`, `seed`, `hash`, and `adversary` are uniformly polynomial-time / strict PPT. -/ +theorem isOraclePPT_prfNonceToPrfDistinguisher + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} {adversary : NonceMACForger} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hadversary : IsOraclePPT (encPair (encPair encBits encBits) encBits) adversary) : + IsOraclePPT encBool (prfNonceToPrfDistinguisher msgLen seed hash adversary) := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hhandler : IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + (encPair encBits (encList (encPair (encPair encBits encBits) encBits))) + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List ((List Bool × List Bool) × List Bool)) => + cwNonceLogHandler msgLen hash p.1.1.1 p.1.2 p.2.1 p.2.2) := by + unfold cwNonceLogHandler + have hcond : ComputableTidilyInPolyTime + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List ((List Bool × List Bool) × List Bool)) => + ((unframe p.2.1.2).length == msgLen p.1.1.1) && + ((dropFrame p.2.1.2).length == p.1.1.1)) + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + encBool := by + polytime + have hyes : IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + (encPair encBits (encList (encPair (encPair encBits encBits) encBits))) + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List ((List Bool × List Bool) × List Bool)) => + (fun pad => + let msg := unframe p.2.1.2 + let nonce := dropFrame p.2.1.2 + let tag := BitString.listXor p.1.1.1 [hash p.1.1.1 p.1.2 msg, pad] + (tag, ((msg, nonce), tag) :: p.2.2)) <$> + (List.take p.1.1.1 <$> ProbOracleComp.query ((), dropFrame p.2.1.2))) := + (IsOraclePPTOn.query_take () (by polytime) (by polytime)).map_with (by polytime) + have hno : IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + (encPair encBits (encList (encPair (encPair encBits encBits) encBits))) + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List ((List Bool × List Bool) × List Bool)) => + pure ([], ((unframe p.2.1.2, dropFrame p.2.1.2), []) :: p.2.2)) := + (show ComputableTidilyInPolyTime + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List ((List Bool × List Bool) × List Bool)) => + (([] : List Bool), + ((unframe p.2.1.2, dropFrame p.2.1.2), ([] : List Bool)) :: p.2.2)) + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + (encPair encBits (encList (encPair (encPair encBits encBits) encBits))) by + polytime).isOraclePPTOn (Operation := Unit) + exact IsOraclePPTOn.cond hcond hyes hno + have hrun : IsOraclePPTOn + (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encPair encBits encBits) encBits) + (encList (encPair (encPair encBits encBits) encBits))) + (fun caller : (ℕ × List Bool) × List Bool => + (OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (cwNonceLogHandler msgLen hash caller.1.1 caller.2)) + (adversary caller.1.1 [])).run []) := by + apply hadversary.run_interpret_preprocess_open + (prepare := fun caller : (ℕ × List Bool) × List Bool => (caller.1.1, ([] : List Bool))) + (initial := fun _ => ([] : List ((List Bool × List Bool) × List Bool))) + (resources := fun caller query => 2 * caller.1.1 + 4 * query.length + 14) + (by fun_prop) hhandler (by fun_prop) + (fun _ _ => True) (fun _ => trivial) (by polytime) + intro caller request queriedTriples _ result hresult + dsimp only [cwNonceLogHandler] at hresult + have hsplit := length_unframe_add_dropFrame_le request.2 + split at hresult + · obtain ⟨pad, -, rfl⟩ := ProbOracleComp.mem_support_map hresult + refine ⟨trivial, ?_, ?_⟩ + · rw [BitString.length_listXor] + lia + · simp only [encList_cons, encPair_apply, encBits_apply, List.length_append, length_frame, + BitString.length_listXor] + lia + · have hres := ProbOracleComp.eq_of_mem_support_pure hresult + subst hres + refine ⟨trivial, ?_, ?_⟩ + · simp + · simp only [encList_cons, encPair_apply, encBits_apply, List.length_append, length_frame, + List.length_nil] + lia + have hk : IsOraclePPTOn (Operation := Unit) (encPair encUnary encBits) encBits + (fun p : ℕ × List Bool => ProbOracleComp.sample (seed p.1)) := + (hseed.preprocess (ComputableInPolyTime.fst _ _)).isOraclePPTOn + have hq : IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encPair encBits encBits) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + encBits + (fun p : ((ℕ × List Bool) × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) => + List.take p.1.1.1 <$> ProbOracleComp.query ((), p.2.1.1.2)) := + IsOraclePPTOn.query_take () (by polytime) (by polytime) + have hpost : ComputableTidilyInPolyTime + (fun p : (((ℕ × List Bool) × List Bool) × + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool))) × + List Bool => + (p.1.2.1.1.1.length == msgLen p.1.1.1.1) && (p.1.2.1.1.2.length == p.1.1.1.1) && + decide (p.1.2.2.map (fun e => e.1.2)).Nodup && !p.1.2.2.contains p.1.2.1 && + (BitString.listXor p.1.1.1.1 + [hash p.1.1.1.1 p.1.1.2 p.1.2.1.1.1, p.2] == p.1.2.1.2)) + (encPair + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encPair encBits encBits) encBits) + (encList (encPair (encPair encBits encBits) encBits)))) + encBits) + encBool := by + polytime + unfold prfNonceToPrfDistinguisher + exact (hk.bind_with (hrun.bind_with (hq.map_with hpost))).isOraclePPT + +/-- Running `prfNonceToPrfDistinguisher msgLen seed hash adversary` in `prfRealGame family` +produces the exact same Boolean distribution as `(carterWegmanNonceMAC ...).sufCmaGame adversary n`. +-/ +theorem eval_prfRealGame_prfNonceToPrfDistinguisher + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) + (adversary : NonceMACForger) (n : ℕ) : + ProbComp.eval (prfRealGame family (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) = + ProbComp.eval + ((carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame + adversary n) := by + let M := carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hfamily + change ProbComp.eval + (prfRealGame family (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) = + ProbComp.eval (M.sufCmaGame adversary n) + simp only [prfRealGame, prfNonceToPrfDistinguisher, NonceMACScheme.sufCmaGame, M, + carterWegmanNonceMAC, Functor.map_map, OracleComp.interpret_bind, OracleComp.interpret_map, + ProbOracleComp.interpret_sample, ProbOracleComp.interpret_query, interpret_unifFin, + ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_pure, + PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_comm (ProbComp.eval (BitString.sampleList n)) (ProbComp.eval (seed n))] + refine PMF.bind_congr_on_support _ _ _ fun k _ => ?_ + refine PMF.bind_congr_on_support _ _ _ fun prfKey hprfKey => ?_ + rw [BitString.eval_sampleList] at hprfKey + have hprfLen : prfKey.length = n := BitString.length_of_mem_support_uniformList hprfKey + rw [interpret_deterministic_run_interpret] + have hhandler : + (fun request state => + OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin (fun req => + pure (prfOracle family n prfKey req.2))) + (cwNonceLogHandler msgLen hash n k request state)) = + M.signingPairOracle (encPair encBits encBits (k, prfKey)) := by + funext request state + simp only [cwNonceLogHandler, NonceMACScheme.signingPairOracle, M, carterWegmanNonceMAC, + encPair_apply, encBits_apply, unframe_frame_append, dropFrame_frame_append, hprfLen] + split + · simp [OracleComp.interpret_map, ProbOracleComp.interpret_query] + · simp + rw [hhandler] + congr 1; funext out + simp only [PMF.pure_map, encPair_apply, encBits_apply, unframe_frame_append, + dropFrame_frame_append, hprfLen] + congr 1 + cases out.1.1.1.length == msgLen n <;> cases out.1.1.2.length == n <;> simp + +open scoped List + +private def toBitTriple (m n : ℕ) + (e : (List Bool × List Bool) × List Bool) : + (BitString m × BitString n) × BitString n := + ((BitString.ofList m e.1.1, BitString.ofList n e.1.2), BitString.ofList n e.2) + +private def ofBitTriple {m n : ℕ} + (e : (BitString m × BitString n) × BitString n) : + (List Bool × List Bool) × List Bool := + ((List.ofFn e.1.1, List.ofFn e.1.2), List.ofFn e.2) + +private theorem ofBitTriple_toBitTriple {m n : ℕ} + {e : (List Bool × List Bool) × List Bool} + (hmsg : e.1.1.length = m) (hnonce : e.1.2.length = n) (htag : e.2.length = n) : + ofBitTriple (toBitTriple m n e) = e := by + rcases e with ⟨⟨msg, nonce⟩, tag⟩ + dsimp only [ofBitTriple, toBitTriple] + rw [BitString.ofFn_ofList hmsg, BitString.ofFn_ofList hnonce, BitString.ofFn_ofList htag] + +private def adaptNonceStep (msgLen : ℕ → ℕ) (n : ℕ) (request : Unit × List Bool) : + StateT (List ((List Bool × List Bool) × List Bool)) + (ProbOracleComp (fun _ : BitString (msgLen n) × BitString n => BitString n)) (List Bool) := + fun queriedTriples => + let msg := unframe request.2 + let nonce := dropFrame request.2 + if (msg.length == msgLen n) && (nonce.length == n) then + (fun t => + let tag := List.ofFn t + (tag, ((msg, nonce), tag) :: queriedTriples)) <$> + ProbOracleComp.query (BitString.ofList (msgLen n) msg, BitString.ofList n nonce) + else + pure ([], ((msg, nonce), []) :: queriedTriples) + +private def cwNonceIdealCheck (msgLen : ℕ → ℕ) + (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (table : BitString n → BitString n) + (out : ((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) : + Bool := + (out.1.1.1.length == msgLen n) && (out.1.1.2.length == n) && + decide (out.2.map (fun e => e.1.2)).Nodup && !out.2.contains out.1 && + (BitString.listXor n + [hash n k out.1.1.1, (randomFunctionOracle n table out.1.1.2).take n] == out.1.2) + +private theorem cwNonceIdealCheck_imp_checkNonceSUF (msgLen : ℕ → ℕ) + (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (table : BitString n → BitString n) + {out : ((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)} + {tr : List ((BitString (msgLen n) × BitString n) × BitString n)} + (hsub : tr.map ofBitTriple <+ out.2.reverse) + (hcheck : cwNonceIdealCheck msgLen hash n k table out = true) : + checkNonceSUF + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table tr (toBitTriple (msgLen n) n out.1) = true := by + simp only [cwNonceIdealCheck, Bool.and_eq_true, Bool.not_eq_true', List.contains_eq_mem, + beq_iff_eq, decide_eq_true_eq, decide_eq_false_iff_not] at hcheck + rcases hcheck with ⟨⟨⟨⟨hmsg, hnonce⟩, hnodup⟩, hnotmem⟩, htag_eq⟩ + have htag_len : out.1.2.length = n := by + rw [← htag_eq, BitString.length_listXor] + have hround : ofBitTriple (toBitTriple (msgLen n) n out.1) = out.1 := + ofBitTriple_toBitTriple hmsg hnonce htag_len + have htr_nodup : (tr.map (fun e => e.1.2)).Nodup := by + have hrev : (out.2.reverse.map (fun e => e.1.2)).Nodup := by + rw [List.map_reverse] + exact List.nodup_reverse.mpr hnodup + have hsub_map : (tr.map (fun e => e.1.2)).map List.ofFn <+ + out.2.reverse.map (fun e => e.1.2) := by + simpa only [List.map_map, Function.comp_def, ofBitTriple] using + hsub.map (fun e => e.1.2) + exact List.Nodup.of_map List.ofFn (hrev.sublist hsub_map) + have htr_notmem : toBitTriple (msgLen n) n out.1 ∉ tr := by + intro hmem + have hmem_map : out.1 ∈ tr.map ofBitTriple := by + rw [← hround] + exact List.mem_map_of_mem hmem + exact hnotmem (List.mem_reverse.mp (hsub.subset hmem_map)) + have hverify : + verify (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k (table (toBitTriple (msgLen n) n out.1).1.2) + (toBitTriple (msgLen n) n out.1).1.1 + (toBitTriple (msgLen n) n out.1).2 = true := by + simp only [verify, toBitTriple, BitString.ofFn_ofList hmsg, decide_eq_true_eq] + have h1 := congrArg (BitString.ofList n) htag_eq + simpa only [randomFunctionOracle, hnonce, ↓reduceIte, BitString.listXor_pair, + ofList_take, BitString.ofList_ofFn] using h1 + simp only [checkNonceSUF, Bool.and_eq_true, Bool.not_eq_true', List.contains_eq_mem, + decide_eq_true_eq, decide_eq_false_iff_not] + exact ⟨⟨htr_nodup, htr_notmem⟩, hverify⟩ + +private theorem eval_cwNonceLogHandler_randomFunctionOracle_le + (msgLen : ℕ → ℕ) (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (table : BitString n → BitString n) + (prog : WordOracleComp Unit ((List Bool × List Bool) × List Bool)) + (init : List ((List Bool × List Bool) × List Bool)) + (tr : List ((BitString (msgLen n) × BitString n) × BitString n)) + (hsub : tr.map ofBitTriple <+ init.reverse) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (fun request state => + ProbComp.eval + (OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin (fun req => + pure (randomFunctionOracle n table req.2))) + (cwNonceLogHandler msgLen hash n k request state)))) + prog).run init).bind + (fun out => PMF.pure (cwNonceIdealCheck msgLen hash n k table out)) true ≤ + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + ((OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptNonceStep msgLen n)) + prog).run init)).run tr).bind + (fun res => + PMF.pure + (checkNonceSUF + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table res.2 (toBitTriple (msgLen n) n res.1.1))) true := by + induction prog using OracleComp.induction generalizing init tr with + | pure a => + simp only [OracleComp.run_interpret_pure, PMF.monad_pure_eq_pure, PMF.pure_bind] + by_cases h : cwNonceIdealCheck msgLen hash n k table (a, init) = true + · rw [h, cwNonceIdealCheck_imp_checkNonceSUF msgLen hash n k table hsub h] + · simp [Bool.eq_false_iff.mpr h] + | query_bind q cont ih => + rw [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + OracleComp.run_interpret_bind] + cases q with + | inl m => + have hsample : + (StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m)) init : + ProbOracleComp (fun _ : BitString (msgLen n) × BitString n => BitString n) + (Fin (m + 1) × List ((List Bool × List Bool) × List Bool))) = + (OracleComp.query (Sum.inl m) >>= fun i => pure (i, init)) := by + simp [StateT.lift, ProbOracleComp.sample, ProbComp.unifFin] + rw [ProbOracleComp.handler, ProbOracleComp.handler, hsample, + OracleComp.run_interpret_bind, OracleComp.run_interpret_query] + simp only [ProbOracleComp.handler, StateT.lift, OracleComp.run_interpret_pure, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + refine bind_apply_mono_on_support (ProbComp.unifOracle m) true fun i _ => ?_ + exact ih i init tr hsub + | inr request => + dsimp only [ProbOracleComp.handler, cwNonceLogHandler, adaptNonceStep] + let msg := unframe request.2 + let nonce := dropFrame request.2 + change (((OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin fun req => + pure (randomFunctionOracle n table req.2)) + (if (msg.length == msgLen n && nonce.length == n) = true then + (fun pad => + let tag := BitString.listXor n [hash n k msg, pad] + (tag, ((msg, nonce), tag) :: init)) <$> + (List.take n <$> ProbOracleComp.query ((), nonce)) + else + pure ([], ((msg, nonce), []) :: init))).eval.bind fun x => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + fun request state => + (OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin fun req => + pure (randomFunctionOracle n table req.2)) + (cwNonceLogHandler msgLen hash n k request state)).eval) + (cont x.1)).run x.2)).bind + fun out => PMF.pure (cwNonceIdealCheck msgLen hash n k table out)) true ≤ + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + (if (msg.length == msgLen n && nonce.length == n) = true then + (fun t => (List.ofFn t, ((msg, nonce), List.ofFn t) :: init)) <$> + ProbOracleComp.query + (BitString.ofList (msgLen n) msg, BitString.ofList n nonce) + else + pure ([], ((msg, nonce), []) :: init))).run tr >>= fun x => + (OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + ((OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptNonceStep msgLen n)) + (cont x.1.1)).run x.1.2)).run x.2).bind + fun res => + PMF.pure + (checkNonceSUF + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table res.2 (toBitTriple (msgLen n) n res.1.1))) true + by_cases hcond : (msg.length == msgLen n && nonce.length == n) = true + · simp only [hcond, ↓reduceIte] + rw [OracleComp.run_interpret_map] + have hq_rhs : + (OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + (ProbOracleComp.query + (BitString.ofList (msgLen n) msg, BitString.ofList n nonce))).run tr = + nonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table (BitString.ofList (msgLen n) msg, BitString.ofList n nonce) tr := + OracleComp.run_interpret_query _ + (Sum.inr (BitString.ofList (msgLen n) msg, BitString.ofList n nonce)) tr + rw [hq_rhs] + simp only [Functor.map_map, OracleComp.interpret_map, ProbOracleComp.interpret_query, + ProbComp.eval_map, ProbComp.eval_pure, nonceFnHandler, + PMF.monad_bind_eq_bind, PMF.monad_map_eq_map, + PMF.pure_map, PMF.pure_bind] + simp only [Bool.and_eq_true, beq_iff_eq] at hcond + rcases hcond with ⟨hmsg, hnonce⟩ + let t := sign + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k (table (BitString.ofList n nonce)) (BitString.ofList (msgLen n) msg) + have htag : List.ofFn t = + BitString.listXor n [hash n k msg, (randomFunctionOracle n table nonce).take n] := by + simp only [t, sign, BitString.ofFn_ofList hmsg, randomFunctionOracle, hnonce, + ↓reduceIte, BitString.listXor_pair, ofList_take, BitString.ofList_ofFn] + rw [← htag] + have hsub' : + (tr ++ [((BitString.ofList (msgLen n) msg, BitString.ofList n nonce), t)]).map + ofBitTriple <+ (((msg, nonce), List.ofFn t) :: init).reverse := by + rw [List.map_append, List.map_singleton, List.reverse_cons] + have he : ofBitTriple ((BitString.ofList (msgLen n) msg, BitString.ofList n nonce), t) = + ((msg, nonce), List.ofFn t) := by + simp [ofBitTriple, BitString.ofFn_ofList hmsg, BitString.ofFn_ofList hnonce] + rw [he] + exact hsub.append (List.Sublist.refl _) + exact ih (List.ofFn t) (((msg, nonce), List.ofFn t) :: init) + (tr ++ [((BitString.ofList (msgLen n) msg, BitString.ofList n nonce), t)]) hsub' + · have hcond' : (msg.length == msgLen n && nonce.length == n) = false := + Bool.eq_false_iff.mpr hcond + simp only [hcond', Bool.false_eq_true, ↓reduceIte, OracleComp.interpret_pure, + ProbComp.eval_pure, StateT.run_pure, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + PMF.pure_bind] + have hsub' : tr.map ofBitTriple <+ (((msg, nonce), []) :: init).reverse := by + rw [List.reverse_cons] + exact hsub.trans (List.sublist_append_left _ _) + exact ih [] (((msg, nonce), []) :: init) tr hsub' + +/-- **Ideal-game bound for `prfNonceToPrfDistinguisher`** ([BonehShoup2023], Section 7.5.1, +Theorem 7.10, p. 274): under `IsDeltaUniversalHash (ProbComp.eval (seed n)) ... ε`, the ideal-game +acceptance probability of `prfNonceToPrfDistinguisher msgLen seed hash adversary` at parameter `n` +is at most `max ε ((2 : ℝ≥0∞) ^ n)⁻¹`. -/ +theorem eval_prfIdealGame_prfNonceToPrfDistinguisher_le + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} {n : ℕ} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) + (adversary : NonceMACForger) : + ProbComp.eval (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) true ≤ + max ε ((2 : ℝ≥0∞) ^ n)⁻¹ := by + let hashBit : List Bool → BitString (msgLen n) → BitString n := + fun k m => BitString.ofList n (hash n k (List.ofFn m)) + let adaptProg : ProbOracleComp (fun _ : BitString (msgLen n) × BitString n => BitString n) + (((List Bool × List Bool) × List Bool) × List ((List Bool × List Bool) × List Bool)) := + (OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptNonceStep msgLen n)) + (adversary n [])).run [] + have hle : + ProbComp.eval (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) true ≤ + ((ProbComp.eval (seed n)).bind fun k => + (PMF.uniformOfFintype (BitString n → BitString n)).bind fun table => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hashBit k table)) + adaptProg).run []).bind fun res => + PMF.pure + (checkNonceSUF hashBit k table res.2 + (toBitTriple (msgLen n) n res.1.1))) true := by + simp only [prfIdealGame, prfNonceToPrfDistinguisher, Functor.map_map, OracleComp.interpret_bind, + OracleComp.interpret_map, ProbOracleComp.interpret_sample, ProbOracleComp.interpret_query, + interpret_unifFin, ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_pure, + ProbComp.eval_uniform, PMF.pure_map] + rw [PMF.bind_comm (PMF.uniformOfFintype (BitString n → BitString n)) (ProbComp.eval (seed n))] + refine bind_apply_mono_on_support (ProbComp.eval (seed n)) true fun k _ => ?_ + refine bind_apply_mono_on_support (PMF.uniformOfFintype (BitString n → BitString n)) true + fun table _ => ?_ + rw [interpret_deterministic_run_interpret, ProbOracleComp.eval_run_interpret] + exact eval_cwNonceLogHandler_randomFunctionOracle_le msgLen hash n k table + (adversary n []) [] [] (List.Sublist.refl []) + refine hle.trans ?_ + have hsim (k : List Bool) : + ((PMF.uniformOfFintype (BitString n → BitString n)).bind fun table => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (nonceFnHandler hashBit k table)) + adaptProg).run []).bind fun res => + PMF.pure + (checkNonceSUF hashBit k table res.2 (toBitTriple (msgLen n) n res.1.1))) = + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + nonceSimHandler) adaptProg).run []).bind fun res => + (PMF.uniformOfFintype (BitString n → BitString n)).bind fun table => + PMF.pure (checkNonceSUF hashBit k (reconstructPadFn hashBit k res.2 table) + res.2 (toBitTriple (msgLen n) n res.1.1))) := by + simpa only [reconstructPadFn_nil] using + probOracleComp_uniform_bind_run_interpret_nonceFnHandler hashBit k adaptProg [] + (fun out tr' padFn => + PMF.pure (checkNonceSUF hashBit k padFn tr' (toBitTriple (msgLen n) n out.1))) + (PMF.pure false) + (fun out tr' padFn hnot => by simp [checkNonceSUF, hnot]) + simp only [hsim] + rw [PMF.bind_comm (ProbComp.eval (seed n)), PMF.bind_apply] + refine tsum_mul_le_of_forall_le _ fun ⟨out, tr⟩ => ?_ + simpa only [BitString.card, Nat.cast_pow, Nat.cast_ofNat] using + seed_uniform_checkNonceSUF_le hh tr (toBitTriple (msgLen n) n out.1) + +/-- **Quantitative SUF-CMA bound for `carterWegmanNonceMAC`** ([BonehShoup2023], Section 7.5.1, +Theorem 7.10, p. 274): at security parameter `n`, the SUF-CMA forgery probability of any +`NonceMACForger` against `carterWegmanNonceMAC` is at most `ε.toReal + (2 ^ n)⁻¹` plus the PRF +distinguishing advantage of `prfNonceToPrfDistinguisher msgLen seed hash adversary`. -/ +theorem sufCmaGame_carterWegmanNonceMAC_toReal_le + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) + {n : ℕ} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) + (hε : ε ≠ ⊤) (adversary : NonceMACForger) : + (ProbComp.eval + ((carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame + adversary n) true).toReal ≤ + ε.toReal + ((2 : ℝ) ^ n)⁻¹ + + (Game.advantage + (ProbComp.eval + (prfRealGame family (prfNonceToPrfDistinguisher msgLen seed hash adversary) n)) + (ProbComp.eval + (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n)) : ℝ) := by + rw [← eval_prfRealGame_prfNonceToPrfDistinguisher hmsgLen hseed hhash hfamily adversary n] + have hinv_ne_top : ((2 : ℝ≥0∞) ^ n)⁻¹ ≠ ⊤ := by simp + have hideal : + (ProbComp.eval + (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) true).toReal ≤ + ε.toReal + ((2 : ℝ) ^ n)⁻¹ := by + have hle := (eval_prfIdealGame_prfNonceToPrfDistinguisher_le hh adversary).trans + (max_le_add_of_nonneg zero_le zero_le) + have htr := ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨hε, hinv_ne_top⟩) hle + simpa only [ENNReal.toReal_add hε hinv_ne_top, ENNReal.toReal_inv, ENNReal.toReal_pow, + ENNReal.toReal_ofNat] using htr + rw [Game.coe_advantage, Game.coe_succProbability, Game.coe_succProbability] + linarith [le_abs_self + ((ProbComp.eval + (prfRealGame family (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) true).toReal - + (ProbComp.eval + (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n) true).toReal)] + +/-- **Asymptotic `NonceMACScheme.SUFCMA` security of `carterWegmanNonceMAC`** +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274): if `family` is a `PseudorandomFunction` +and `(seed n, hash n)` is an `(ε n)`-almost-Δ-universal hash family on `BitString (msgLen n)` into +`BitString n` with `Negligible ε`, then `carterWegmanNonceMAC` satisfies `NonceMACScheme.SUFCMA`. -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.sufCma_carterWegmanNonceMAC + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + {ε : ℕ → ℝ≥0} + (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) (ε n)) + (hε : Negligible ε) : + (carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hprf.polyTime).SUFCMA := by + refine NonceMACScheme.SUFCMA.of_negligible fun adversary hadversary => ?_ + have hgeom : Negligible (fun n => ((2 : ℝ≥0) ^ n)⁻¹) := by + simpa only [inv_pow] using negligible_geometric (ratio := 2⁻¹) (by norm_num) + have hdist := hprf.secure (prfNonceToPrfDistinguisher msgLen seed hash adversary) + (isOraclePPT_prfNonceToPrfDistinguisher hmsgLen hseed hhash hadversary) + refine negligible_of_le ((hε.add hgeom).add hdist) fun n => ?_ + rw [← NNReal.coe_le_coe, Game.coe_succProbability] + simp only [Pi.add_apply, NNReal.coe_add, NNReal.coe_inv, NNReal.coe_pow, NNReal.coe_ofNat] + simpa only [ENNReal.coe_toReal] using + sufCmaGame_carterWegmanNonceMAC_toReal_le hmsgLen hseed hhash hprf.polyTime + (hh n) ENNReal.coe_ne_top adversary + +/-- **Asymptotic `NonceMACScheme.EUFCMA` security of `carterWegmanNonceMAC`** +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274). -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.eufCma_carterWegmanNonceMAC + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + {ε : ℕ → ℝ≥0} + (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) (ε n)) + (hε : Negligible ε) : + (carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hprf.polyTime).EUFCMA := + (hprf.sufCma_carterWegmanNonceMAC hmsgLen hseed hhash hh hε).eufCma + end Nonce /-! ### Randomized Carter–Wegman MAC (Boneh–Shoup Section 7.4, Theorem 7.9) -/ @@ -2621,20 +3605,20 @@ theorem uniform_bind_run_interpret_randomNonceFnHandler {α β : Type} post res.1 res.2 (reconstructPadFn hash k res.2 table)) := by have happ_fn (padFn : N → Y) : ∀ m tr₁ res, res ∈ (randomNonceFnHandler hash k padFn m tr₁).support → - ∃ e, res.2 = tr₁ ++ [e] := by + ∃ s, res.2 = tr₁ ++ s := by intro m tr₁ res hres simp only [randomNonceFnHandler, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, Set.mem_singleton_iff] at hres rcases hres with ⟨x, -, hres⟩ - exact ⟨((m, x), _), congrArg Prod.snd hres⟩ + exact ⟨[((m, x), _)], congrArg Prod.snd hres⟩ have happ_sim : ∀ m tr₁ res, res ∈ (randomNonceSimHandler (M := M) (N := N) (Y := Y) m tr₁).support → - ∃ e, res.2 = tr₁ ++ [e] := by + ∃ s, res.2 = tr₁ ++ s := by intro m tr₁ res hres simp only [randomNonceSimHandler, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, Set.mem_singleton_iff] at hres rcases hres with ⟨x, -, t, -, hres⟩ - exact ⟨((m, x), t), congrArg Prod.snd hres⟩ + exact ⟨[((m, x), t)], congrArg Prod.snd hres⟩ have hpost_sim : ∀ a tr', ¬ (tr'.map (fun e => e.1.2)).Nodup → ((PMF.uniformOfFintype (N → Y)).bind fun table => post a tr' (reconstructPadFn hash k tr' table)) = c := by @@ -3215,6 +4199,1347 @@ theorem _root_.Cslib.Crypto.PseudorandomFunction.negligible_prfRandomNonceGame (maskedRandomNonceGame_le_maskedRandomNonceStrongGame (seed n) (prfFnDist family n) (hash n) (forger n)) +omit [DecidableEq M] [DecidableEq Y] in +/-- **Multi-query simulation equivalence for `randomNonceFnHandler` on `ProbOracleComp` programs +under a random function**: lifting `uniform_bind_run_interpret_randomNonceFnHandler` to programs +that also draw private coins via `ProbComp.unifOracle`. -/ +theorem probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler {α β : Type} + (hash : K → M → Y) (k : K) + (prog : ProbOracleComp (fun _ : M => N × Y) α) (tr : List ((M × N) × Y)) + (post : α → List ((M × N) × Y) → (N → Y) → PMF β) (c : PMF β) + (hpost : ∀ a tr' padFn, ¬ (tr'.map (fun e => e.1.2)).Nodup → post a tr' padFn = c) : + ((PMF.uniformOfFintype (N → Y)).bind fun table => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k (reconstructPadFn hash k tr table))) + prog).run tr).bind + fun res => post res.1 res.2 (reconstructPadFn hash k tr table)) = + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) prog).run tr).bind fun res => + (PMF.uniformOfFintype (N → Y)).bind fun table => + post res.1 res.2 (reconstructPadFn hash k res.2 table)) := by + have happ_fn (padFn : N → Y) : + ∀ q tr₁ res, + res ∈ (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k padFn) q tr₁).support → + ∃ s, res.2 = tr₁ ++ s := by + intro q tr₁ res hres + cases q with + | inl num => + simp only [ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨i, -, hres⟩ + exact ⟨[], by simp [congrArg Prod.snd hres]⟩ + | inr m => + simp only [ProbOracleComp.handler, randomNonceFnHandler, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨x, -, hres⟩ + exact ⟨[((m, x), _)], congrArg Prod.snd hres⟩ + have happ_sim : + ∀ q tr₁ res, + res ∈ (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceSimHandler (M := M) (N := N) (Y := Y)) q tr₁).support → + ∃ s, res.2 = tr₁ ++ s := by + intro q tr₁ res hres + cases q with + | inl num => + simp only [ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨i, -, hres⟩ + exact ⟨[], by simp [congrArg Prod.snd hres]⟩ + | inr m => + simp only [ProbOracleComp.handler, randomNonceSimHandler, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.mem_support_bind_iff, PMF.support_pure, + Set.mem_singleton_iff] at hres + rcases hres with ⟨x, -, t, -, hres⟩ + exact ⟨[((m, x), t)], congrArg Prod.snd hres⟩ + have hpost_sim : ∀ a tr', ¬ (tr'.map (fun e => e.1.2)).Nodup → + ((PMF.uniformOfFintype (N → Y)).bind fun table => + post a tr' (reconstructPadFn hash k tr' table)) = c := by + intro a tr' hnot + simp only [hpost a tr' _ hnot, PMF.bind_const] + induction prog using OracleComp.induction generalizing tr with + | pure a => + simp [PMF.monad_pure_eq_pure] + | query_bind q cont ih => + cases q with + | inl num => + simp only [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, + PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_comm (PMF.uniformOfFintype (N → Y)) (ProbComp.unifOracle num)] + congr 1; funext i + exact ih i tr + | inr m => + by_cases hnodup : (tr.map (fun e => e.1.2)).Nodup + · simp only [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + ProbOracleComp.handler, randomNonceFnHandler, randomNonceSimHandler, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_comm (PMF.uniformOfFintype (N → Y)) (PMF.uniformOfFintype N)] + congr 1; funext x + by_cases hx : x ∈ tr.map (fun e => e.1.2) + · have hnot (t : Y) : ¬ ((tr ++ [((m, x), t)]).map (fun e => e.1.2)).Nodup := + not_nodup_map_append_of_mem m t hx + have hlhs (table : N → Y) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k (reconstructPadFn hash k tr table))) + (cont (x, sign hash k (reconstructPadFn hash k tr table x) m))).run + (tr ++ [((m, x), sign hash k (reconstructPadFn hash k tr table x) m)])).bind + (fun res => post res.1 res.2 (reconstructPadFn hash k tr table)) = c := + run_interpret_bind_of_not_nodup _ (happ_fn _) _ (hnot _) _ c + (fun a tr' h => hpost a tr' _ h) + have hrhs (t : Y) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (cont (x, t))).run + (tr ++ [((m, x), t)])).bind + (fun res => (PMF.uniformOfFintype (N → Y)).bind fun table => + post res.1 res.2 (reconstructPadFn hash k res.2 table)) = c := + run_interpret_bind_of_not_nodup _ happ_sim _ (hnot t) _ c hpost_sim + simp only [hlhs, hrhs, PMF.bind_const] + · rw [uniform_reconstructPadFn_step hash k m hx + (fun t tr' fn => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k fn)) (cont (x, t))).run tr').bind + fun res => post res.1 res.2 fn)] + congr 1; funext t + exact ih (x, t) (tr ++ [((m, x), t)]) + · have hlhs (table : N → Y) : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k (reconstructPadFn hash k tr table))) + (OracleComp.query (Sum.inr m) >>= cont)).run tr).bind + (fun res => post res.1 res.2 (reconstructPadFn hash k tr table)) = c := + run_interpret_bind_of_not_nodup _ (happ_fn _) _ hnodup _ c + (fun a tr' h => hpost a tr' _ h) + have hrhs : + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (OracleComp.query (Sum.inr m) >>= cont)).run tr).bind + (fun res => (PMF.uniformOfFintype (N → Y)).bind fun table => + post res.1 res.2 (reconstructPadFn hash k res.2 table)) = c := + run_interpret_bind_of_not_nodup _ happ_sim _ hnodup _ c hpost_sim + simp only [hlhs, hrhs, PMF.bind_const] + +omit [AddGroup Y] [DecidableEq M] [DecidableEq Y] in +/-- Birthday-collision bound for `randomNonceSimHandler` on `ProbOracleComp` programs: starting +from `tr`, any `Q`-query-bounded `ProbOracleComp` program produces a transcript with a repeated +nonce with probability at most +`((∑ i ∈ Finset.range Q, (tr.length + i) : ℕ) : ℝ≥0∞) / Fintype.card N` when +`(tr.map (fun e => e.1.2)).Nodup`, and at most `1` otherwise. -/ +theorem probOracleComp_randomNonceSimHandler_not_nodup_le {α : Type} + {prog : ProbOracleComp (fun _ : M => N × Y) α} {Q : ℕ} + (hprog : prog.IsQueryBounded Q) (tr : List ((M × N) × Y)) : + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) prog).run tr).bind fun res => + PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ + if (tr.map (fun e => e.1.2)).Nodup then + ((∑ i ∈ Finset.range Q, (tr.length + i) : ℕ) : ℝ≥0∞) / Fintype.card N + else 1 := by + induction hprog generalizing tr with + | pure a Q => + by_cases hnodup : (tr.map (fun e => e.1.2)).Nodup <;> + simp [hnodup, PMF.monad_pure_eq_pure] + | liftBind q cont Q hcont ih => + cases q with + | inl num => + simp only [Sum.elim_inl, Nat.add_zero] + change (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (OracleComp.query (Sum.inl num) >>= cont)).run tr).bind + fun res => PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ _ + simp only [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + ProbOracleComp.handler, StateT.lift, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + PMF.bind_bind, PMF.pure_bind] + rw [PMF.bind_apply] + exact tsum_mul_le_of_forall_le (ProbComp.unifOracle num) fun i => ih i tr + | inr m => + simp only [Sum.elim_inr] + change (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (OracleComp.query (Sum.inr m) >>= cont)).run tr).bind + fun res => PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ _ + by_cases hnodup : (tr.map (fun e => e.1.2)).Nodup + · simp only [hnodup, ↓reduceIte, OracleComp.run_interpret_bind, + OracleComp.run_interpret_query, ProbOracleComp.handler, randomNonceSimHandler, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + let B : ℝ≥0∞ := + ((∑ i ∈ Finset.range Q, (tr.length + 1 + i) : ℕ) : ℝ≥0∞) / Fintype.card N + have hxt (x : N) (t : Y) : + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (cont (x, t))).run + (tr ++ [((m, x), t)])).bind fun res => + PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ + (PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B := by + by_cases hx : x ∈ tr.map (fun e => e.1.2) + · simp only [decide_eq_true hx, PMF.pure_apply, ↓reduceIte] + exact (PMF.coe_le_one _ _).trans le_self_add + · have hnodup' : ((tr ++ [((m, x), t)]).map (fun e => e.1.2)).Nodup := by + rw [List.map_append, List.map_singleton, List.nodup_append] + refine ⟨hnodup, List.nodup_singleton _, fun a ha b hb hab => ?_⟩ + rw [List.mem_singleton] at hb + subst hb; subst hab + exact hx ha + have hih := ih (x, t) (tr ++ [((m, x), t)]) + simp only [hnodup', ↓reduceIte, List.length_append, List.length_singleton] at hih + simp only [decide_eq_false hx, PMF.pure_apply, Bool.true_eq_false, ↓reduceIte, + zero_add] + exact hih + have hx_bound (x : N) : + ((PMF.uniformOfFintype Y).bind fun t => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (cont (x, t))).run + (tr ++ [((m, x), t)])).bind fun res => + PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true ≤ + (PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B := by + rw [PMF.bind_apply] + exact tsum_mul_le_of_forall_le (PMF.uniformOfFintype Y) (hxt x) + have hmem_le : + ((PMF.uniformOfFintype N).bind fun x => + PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true ≤ + (tr.length : ℝ≥0∞) / Fintype.card N := by + let s : Set N := {x | x ∈ tr.map (fun e => e.1.2)} + have h_eq : + ((PMF.uniformOfFintype N).bind fun x => + PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true = + (PMF.uniformOfFintype N).toOuterMeasure s := by + rw [PMF.bind_apply, PMF.toOuterMeasure_apply] + change ∑' x, PMF.uniformOfFintype N x * (PMF.pure (decide (x ∈ s))) true = + ∑' x, s.indicator (PMF.uniformOfFintype N) x + refine tsum_congr fun x => ?_ + by_cases hx : x ∈ s <;> simp [hx] + rw [h_eq, Probability.PMF.toOuterMeasure_uniformOfFintype, div_eq_mul_inv] + gcongr + have hsub : Finset.univ.filter (· ∈ s) ⊆ (tr.map (fun e => e.1.2)).toFinset := by + intro x hx + rw [Finset.mem_filter] at hx + exact List.mem_toFinset.mpr hx.2 + have hcard : (Finset.univ.filter (· ∈ s)).card ≤ tr.length := + (Finset.card_le_card hsub).trans + ((List.toFinset_card_le _).trans (by simp)) + exact_mod_cast hcard + rw [PMF.bind_apply] + calc ∑' x, PMF.uniformOfFintype N x * + ((PMF.uniformOfFintype Y).bind fun t => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) (cont (x, t))).run + (tr ++ [((m, x), t)])).bind fun res => + PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + ≤ ∑' x, PMF.uniformOfFintype N x * + ((PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B) := + ENNReal.tsum_le_tsum fun x => mul_le_mul_of_nonneg_left (hx_bound x) zero_le + _ = ((PMF.uniformOfFintype N).bind fun x => + PMF.pure (decide (x ∈ tr.map (fun e => e.1.2)))) true + B := by + simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, + (PMF.uniformOfFintype N).tsum_coe, one_mul, PMF.bind_apply] + _ ≤ (tr.length : ℝ≥0∞) / Fintype.card N + B := add_le_add hmem_le le_rfl + _ = ((∑ i ∈ Finset.range (Q + 1), (tr.length + i) : ℕ) : ℝ≥0∞) / Fintype.card N := by + dsimp only [B] + rw [← ENNReal.add_div, ← Nat.cast_add] + congr 2 + rw [Finset.sum_range_succ', Nat.add_zero, add_comm (tr.length)] + congr 1 + refine Finset.sum_congr rfl fun i _ => by omega + · simp only [hnodup, ↓reduceIte] + exact PMF.coe_le_one _ _ + +/-- **Ideal randomized Carter–Wegman SUF-CMA bound for `ProbOracleComp` programs**: +under `IsDeltaUniversalHash seed hash ε`, any `Q`-query-bounded `ProbOracleComp` program `prog` +against `randomNonceFnHandler` satisfies `checkRandomNonceSUF` on `out res.1` with probability at +most `(Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) + (Fintype.card Y : ℝ≥0∞)⁻¹ + ε`. -/ +theorem seed_uniform_probOracleComp_checkRandomNonceSUF_le {α : Type} + {seed : PMF K} {hash : K → M → Y} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash seed hash ε) + {prog : ProbOracleComp (fun _ : M => N × Y) α} {Q : ℕ} + (hprog : prog.IsQueryBounded Q) (out : α → (M × N) × Y) : + (seed.bind fun k => + (PMF.uniformOfFintype (N → Y)).bind fun rf => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k rf)) + prog).run []).bind + fun res => PMF.pure (checkRandomNonceSUF hash k rf res.2 (out res.1))) true ≤ + (Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) + (Fintype.card Y : ℝ≥0∞)⁻¹ + ε := by + have hmono : + (seed.bind fun k => + (PMF.uniformOfFintype (N → Y)).bind fun rf => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k rf)) + prog).run []).bind + fun res => PMF.pure (checkRandomNonceSUF hash k rf res.2 (out res.1))) true ≤ + (seed.bind fun k => + (PMF.uniformOfFintype (N → Y)).bind fun rf => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k rf)) + prog).run []).bind + fun res => + PMF.pure (checkRandomNonceOrCollision hash k rf res.2 (out res.1))) true := by + refine bind_apply_mono_on_support seed true fun k _ => ?_ + refine bind_apply_mono_on_support (PMF.uniformOfFintype (N → Y)) true fun rf _ => ?_ + refine bind_apply_mono_on_support + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k rf)) + prog).run []) true fun res _ => ?_ + by_cases h : checkRandomNonceSUF hash k rf res.2 (out res.1) = true + · rw [h, checkRandomNonceSUF_imp_checkRandomNonceOrCollision hash k rf res.2 (out res.1) h] + · simp [Bool.eq_false_iff.mpr h] + refine hmono.trans ?_ + have hsim (k : K) : + ((PMF.uniformOfFintype (N → Y)).bind fun rf => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hash k rf)) + prog).run []).bind + fun res => PMF.pure (checkRandomNonceOrCollision hash k rf res.2 (out res.1))) = + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) prog).run []).bind fun res => + (PMF.uniformOfFintype (N → Y)).bind fun table => + PMF.pure + (checkRandomNonceOrCollision hash k + (reconstructPadFn hash k res.2 table) res.2 (out res.1))) := by + simpa only [reconstructPadFn_nil] using + probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler hash k prog [] + (fun a tr' padFn => PMF.pure (checkRandomNonceOrCollision hash k padFn tr' (out a))) + (PMF.pure true) + (fun a tr' padFn hnot => by simp [checkRandomNonceOrCollision, hnot]) + simp only [hsim] + let simPMF := + (OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + randomNonceSimHandler) prog).run [] + rw [PMF.bind_comm seed simPMF] + have hpoint (res : α × List ((M × N) × Y)) : + (seed.bind fun k => + (PMF.uniformOfFintype (N → Y)).bind fun table => + PMF.pure + (checkRandomNonceOrCollision hash k + (reconstructPadFn hash k res.2 table) res.2 (out res.1))) true ≤ + (PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by + by_cases hnodup : (res.2.map (fun e => e.1.2)).Nodup + · have heq (k : K) (table : N → Y) : + checkRandomNonceOrCollision hash k + (reconstructPadFn hash k res.2 table) res.2 (out res.1) = + checkNonceSUF hash k (reconstructPadFn hash k res.2 table) res.2 (out res.1) := by + simp [checkRandomNonceOrCollision, hnodup] + simp only [heq, decide_eq_true hnodup, Bool.not_true, PMF.pure_apply, Bool.true_eq_false, + ↓reduceIte, zero_add] + exact seed_uniform_checkNonceSUF_le hh res.2 (out res.1) + · simp only [decide_eq_false hnodup, Bool.not_false, PMF.pure_apply, ↓reduceIte] + exact (PMF.coe_le_one _ _).trans le_self_add + have hsum_nat : 2 * (∑ i ∈ Finset.range Q, i) ≤ Q ^ 2 := by + rw [Finset.sum_range_id, sq] + exact (Nat.mul_div_le (Q * (Q - 1)) 2).trans (Nat.mul_le_mul_left Q (Nat.sub_le Q 1)) + have hsum : ((∑ i ∈ Finset.range Q, i : ℕ) : ℝ≥0∞) / Fintype.card N ≤ + (Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) := by + rw [← ENNReal.mul_div_mul_left _ _ (by norm_num : (2 : ℝ≥0∞) ≠ 0) ENNReal.ofNat_ne_top] + gcongr + exact_mod_cast hsum_nat + have hmax : max ε (Fintype.card Y : ℝ≥0∞)⁻¹ ≤ (Fintype.card Y : ℝ≥0∞)⁻¹ + ε := by + rw [add_comm] + exact max_le_add_of_nonneg zero_le zero_le + rw [add_assoc, PMF.bind_apply] + calc ∑' res, simPMF res * + (seed.bind fun k => + (PMF.uniformOfFintype (N → Y)).bind fun table => + PMF.pure + (checkRandomNonceOrCollision hash k + (reconstructPadFn hash k res.2 table) res.2 (out res.1))) true + ≤ ∑' res, simPMF res * + ((PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + + max ε (Fintype.card Y : ℝ≥0∞)⁻¹) := + ENNReal.tsum_le_tsum fun res => mul_le_mul_of_nonneg_left (hpoint res) zero_le + _ = (simPMF.bind fun res => + PMF.pure (!decide (res.2.map (fun e => e.1.2)).Nodup)) true + + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by + simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, simPMF.tsum_coe, one_mul, + PMF.bind_apply] + _ ≤ ((∑ i ∈ Finset.range Q, i : ℕ) : ℝ≥0∞) / Fintype.card N + + max ε (Fintype.card Y : ℝ≥0∞)⁻¹ := by + refine add_le_add ?_ le_rfl + have hcol := probOracleComp_randomNonceSimHandler_not_nodup_le hprog [] + simpa using hcol + _ ≤ (Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) + ((Fintype.card Y : ℝ≥0∞)⁻¹ + ε) := + add_le_add hsum hmax + +/-! #### Word-level `MACScheme` packaging and `IsOraclePPT` PRF reduction (Theorem 7.9) -/ + +/-- **Computational randomized Carter–Wegman MAC (`MACScheme`)** +([BonehShoup2023], Section 7.4, Theorem 7.9, pp. 267–270): +given a polynomial-time message-length schedule `msgLen : ℕ → ℕ`, a strict-PPT hash-key sampler +`seed : ℕ → ProbComp (List Bool)`, a polynomial-time hash evaluator +`hash : ℕ → List Bool → List Bool → List Bool`, and a polynomial-time PRF family +`family : List Bool → List Bool → List Bool`: +* `keyGen n` samples `k ← seed n` and `prfKey ← BitString.sampleList n`, returning the framed pair + `encPair encBits encBits (k, prfKey)`. +* `sign sk msg` recovers `k := unframe sk`, `prfKey := dropFrame sk`, and `n := prfKey.length`, + samples a fresh uniform `n`-bit nonce `nonce ← BitString.sampleList n`, and when + `msg.length == msgLen n` returns the framed pair `encPair encBits encBits (nonce, tag)` where + `tag = BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n]` (and `[]` + otherwise). +* `verify sk msg fullTag` decodes `nonce := unframe fullTag`, computes the expected `n`-bit tag + `tag := BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n]`, and checks + `msg.length == msgLen n`, `nonce.length == n`, and + `encPair encBits encBits (nonce, tag) == fullTag`. -/ +noncomputable def carterWegmanRandomMAC (msgLen : ℕ → ℕ) + (seed : ℕ → ProbComp (List Bool)) + (hash : ℕ → List Bool → List Bool → List Bool) + (family : List Bool → List Bool → List Bool) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) : MACScheme where + msgLen := msgLen + msgLen_polyTime := hmsgLen + keyGen n := do + let k ← seed n + let prfKey ← BitString.sampleList n + return encPair encBits encBits (k, prfKey) + sign sk msg := do + let nonce ← BitString.sampleList (dropFrame sk).length + let k := unframe sk + let prfKey := dropFrame sk + let n := prfKey.length + return if msg.length == msgLen n then + encPair encBits encBits + (nonce, BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n]) + else + [] + verify sk msg fullTag := + let k := unframe sk + let prfKey := dropFrame sk + let n := prfKey.length + let nonce := unframe fullTag + let tag := BitString.listXor n [hash n k msg, (prfOracle family n prfKey nonce).take n] + (msg.length == msgLen n) && (nonce.length == n) && + (encPair encBits encBits (nonce, tag) == fullTag) + keyGen_ppt := by ppt + sign_ppt := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hfamily_tidy := hfamily.tidy + have hprf : ComputableTidilyInPolyTime + (fun p : (List Bool × List Bool) × List Bool => + prfOracle family (dropFrame p.1.1).length (dropFrame p.1.1) p.2) + (encPair (encPair encBits encBits) encBits) encBits := by + have heq : (fun p : (List Bool × List Bool) × List Bool => + prfOracle family (dropFrame p.1.1).length (dropFrame p.1.1) p.2) = + (fun p : (List Bool × List Bool) × List Bool => + if p.2.length == (dropFrame p.1.1).length then + family (dropFrame p.1.1) p.2 + else + []) := by + funext p + simp [prfOracle] + rw [heq] + polytime + have hbody : ComputableTidilyInPolyTime + (fun p : (List Bool × List Bool) × List Bool => + let k := unframe p.1.1 + let prfKey := dropFrame p.1.1 + let n := prfKey.length + if p.1.2.length == msgLen n then + encPair encBits encBits + (p.2, BitString.listXor n [hash n k p.1.2, (prfOracle family n prfKey p.2).take n]) + else + []) + (encPair (encPair encBits encBits) encBits) encBits := by + polytime + exact (ComputableInPolyTime.sampleList (by polytime)).bind_with hbody.isPPTOn + verify_polyTime := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hfamily_tidy := hfamily.tidy + have hprf : ComputableTidilyInPolyTime + (fun p : List Bool × List Bool × List Bool => + prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe p.2.2)) + (encPair encBits (encPair encBits encBits)) encBits := by + have heq : (fun p : List Bool × List Bool × List Bool => + prfOracle family (dropFrame p.1).length (dropFrame p.1) (unframe p.2.2)) = + (fun p : List Bool × List Bool × List Bool => + if (unframe p.2.2).length == (dropFrame p.1).length then + family (dropFrame p.1) (unframe p.2.2) + else + []) := by + funext p + simp [prfOracle] + rw [heq] + polytime + exact .of_tidy (by polytime) + verify_sign := by + intro n sk hsk msg hmsg fullTag htag + simp only [ProbComp.eval_bind, ProbComp.eval_pure, BitString.eval_sampleList, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hsk htag + rcases hsk with ⟨k, -, prfKey, hprfKey, rfl⟩ + have hprfLen : prfKey.length = n := BitString.length_of_mem_support_uniformList hprfKey + rcases htag with ⟨nonce, hnonce, rfl⟩ + simp only [encPair_apply, encBits_apply, dropFrame_frame_append, unframe_frame_append, + hprfLen, hmsg, beq_self_eq_true, ↓reduceIte] at hnonce ⊢ + have hnonceLen : nonce.length = n := BitString.length_of_mem_support_uniformList hnonce + simp [hnonceLen] + +/-- Open stateful handler for the randomized Carter–Wegman PRF reduction +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): given the hash key `k` and a signing request +`msg := request.2`, when `msg.length == msgLen n` it samples a fresh uniform `n`-bit nonce +`nonce ← BitString.sampleList n`, queries the external oracle on `((), nonce)` (reading `n` bits +`pad`), computes `tag := BitString.listXor n [hash n k msg, pad]` and +`fullTag := encPair encBits encBits (nonce, tag)`, and prepends `(msg, fullTag)` to `queriedPairs`; +otherwise it returns `[]` and prepends `(msg, [])` without querying the external oracle. -/ +noncomputable def cwRandomNonceLogHandler (msgLen : ℕ → ℕ) + (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (request : Unit × List Bool) : + StateT (List (List Bool × List Bool)) (WordOracleComp Unit) (List Bool) := + fun queriedPairs => + let msg := request.2 + if msg.length == msgLen n then do + let nonce ← ProbOracleComp.sample (BitString.sampleList n) + (fun pad => + let tag := BitString.listXor n [hash n k msg, pad] + let fullTag := encPair encBits encBits (nonce, tag) + (fullTag, (msg, fullTag) :: queriedPairs)) <$> + (List.take n <$> ProbOracleComp.query ((), nonce)) + else + pure ([], (msg, []) :: queriedPairs) + +/-- Oracle reduction turning an adaptive word-level `Forger` into an `OracleDistinguisher` +for the PRF security game ([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): +1. Sample `k ← seed n`. +2. Run `adversary n []`, answering each signing query via `cwRandomNonceLogHandler msgLen hash n k`. +3. Query the external oracle on the candidate nonce `unframe out.1.2` (reading `n` bits `pad`), and + accept iff `msg.length == msgLen n`, `(unframe fullTag).length == n`, the candidate + `(msg, fullTag)` pair was not returned by the signing oracle, and + `encPair encBits encBits (unframe fullTag, BitString.listXor n [hash n k msg, pad]) == fullTag`. +-/ +noncomputable def prfRandomNonceToPrfDistinguisher (msgLen : ℕ → ℕ) + (seed : ℕ → ProbComp (List Bool)) + (hash : ℕ → List Bool → List Bool → List Bool) (adversary : Forger) : + OracleDistinguisher := fun n _ => do + let k ← ProbOracleComp.sample (seed n) + let out ← + (OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (cwRandomNonceLogHandler msgLen hash n k)) + (adversary n [])).run [] + (fun pad => + let msg := out.1.1 + let fullTag := out.1.2 + let nonce := unframe fullTag + let tag := BitString.listXor n [hash n k msg, pad] + (msg.length == msgLen n) && (nonce.length == n) && !out.2.contains out.1 && + (encPair encBits encBits (nonce, tag) == fullTag)) <$> + (List.take n <$> ProbOracleComp.query ((), unframe out.1.2)) + +private theorem isOraclePPTOn_cwRandomNonceLogHandler + {msgLen : ℕ → ℕ} {hash : ℕ → List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) : + IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + (encPair encBits (encList (encPair encBits encBits))) + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool)) => + cwRandomNonceLogHandler msgLen hash p.1.1.1 p.1.2 p.2.1 p.2.2) := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hframe : ComputableTidilyInPolyTime frame encBits encBits := + ComputableInPolyTime.frame.tidy + unfold cwRandomNonceLogHandler + have hcond : ComputableTidilyInPolyTime + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool)) => + p.2.1.2.length == msgLen p.1.1.1) + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + encBool := by + polytime + have hsample : IsOraclePPTOn (Operation := Unit) + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + encBits + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool)) => + ProbOracleComp.sample (BitString.sampleList p.1.1.1)) := + (ComputableInPolyTime.sampleList (by polytime)).isOraclePPTOn + let mkFullTag (r : ((((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool))) × List Bool) × List Bool) : + List Bool := + frame r.1.2 ++ BitString.listXor r.1.1.1.1.1 [hash r.1.1.1.1.1 r.1.1.1.2 r.1.1.2.1.2, r.2] + have hmkFullTag : ComputableInPolyTime mkFullTag + (encPair + (encPair + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + encBits) + encBits) + encBits := by + unfold mkFullTag + polytime + have hpost : ComputableTidilyInPolyTime + (fun r : ((((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool))) × List Bool) × List Bool => + (mkFullTag r, (r.1.1.2.1.2, mkFullTag r) :: r.1.1.2.2)) + (encPair + (encPair + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + encBits) + encBits) + (encPair encBits (encList (encPair encBits encBits))) := by + refine ComputableInPolyTime.tidy ?_ + exact ComputableInPolyTime.prod hmkFullTag + (ComputableInPolyTime.cons' + (ComputableInPolyTime.prod (by polytime) hmkFullTag) + (by polytime)) + have hquery : IsOraclePPTOn + (encPair + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + encBits) + (encPair encBits (encList (encPair encBits encBits))) + (fun q : (((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool))) × List Bool => + (fun pad => + let msg := q.1.2.1.2 + let nonce := q.2 + let tag := BitString.listXor q.1.1.1.1 [hash q.1.1.1.1 q.1.1.2 msg, pad] + let fullTag := encPair encBits encBits (nonce, tag) + (fullTag, (msg, fullTag) :: q.1.2.2)) <$> + (List.take q.1.1.1.1 <$> ProbOracleComp.query ((), q.2))) := + (IsOraclePPTOn.query_take () (by polytime) (by polytime)).map_with hpost + have hyes : IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + (encPair encBits (encList (encPair encBits encBits))) + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool)) => do + let nonce ← ProbOracleComp.sample (BitString.sampleList p.1.1.1) + (fun pad => + let msg := p.2.1.2 + let tag := BitString.listXor p.1.1.1 [hash p.1.1.1 p.1.2 msg, pad] + let fullTag := encPair encBits encBits (nonce, tag) + (fullTag, (msg, fullTag) :: p.2.2)) <$> + (List.take p.1.1.1 <$> ProbOracleComp.query ((), nonce))) := + hsample.bind_with hquery + have hno : IsOraclePPTOn (Operation := Unit) + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + (encPair encBits (encList (encPair encBits encBits))) + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool)) => + pure ([], (p.2.1.2, []) :: p.2.2)) := + (show ComputableTidilyInPolyTime + (fun p : ((ℕ × List Bool) × List Bool) × + ((Unit × List Bool) × List (List Bool × List Bool)) => + (([] : List Bool), (p.2.1.2, ([] : List Bool)) :: p.2.2)) + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair (encFinite Unit) encBits) + (encList (encPair encBits encBits)))) + (encPair encBits (encList (encPair encBits encBits))) by + polytime).isOraclePPTOn (Operation := Unit) + exact IsOraclePPTOn.cond hcond hyes hno + +private theorem isOraclePPTOn_cwRandomNonceCheck + {msgLen : ℕ → ℕ} {hash : ℕ → List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) : + IsOraclePPTOn + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair encBits encBits) (encList (encPair encBits encBits)))) + encBool + (fun p : ((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool)) => + (fun pad => + let msg := p.2.1.1 + let fullTag := p.2.1.2 + let nonce := unframe fullTag + let tag := BitString.listXor p.1.1.1 [hash p.1.1.1 p.1.2 msg, pad] + (msg.length == msgLen p.1.1.1) && (nonce.length == p.1.1.1) && + !p.2.2.contains p.2.1 && + (encPair encBits encBits (nonce, tag) == fullTag)) <$> + (List.take p.1.1.1 <$> ProbOracleComp.query ((), unframe p.2.1.2))) := by + have hmsgLen_tidy := hmsgLen.tidy + have hhash_tidy := hhash.tidy + have hunframe : ComputableTidilyInPolyTime unframe encBits encBits := + ComputableInPolyTime.unframe.tidy + let encR := + encPair + (encPair (encPair (encPair encUnary encBits) encBits) + (encPair (encPair encBits encBits) (encList (encPair encBits encBits)))) + encBits + let expectedFullTag (r : (((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool))) × List Bool) : List Bool := + frame (unframe r.1.2.1.2) ++ + BitString.listXor r.1.1.1.1 [hash r.1.1.1.1 r.1.1.2 r.1.2.1.1, r.2] + have hexpected : ComputableTidilyInPolyTime expectedFullTag encR encBits := + ComputableTidilyInPolyTime.bitsAppend + (ComputableInPolyTime.frame.tidy.comp (hunframe.comp (by polytime))) + (by polytime) + have hc1 : ComputableTidilyInPolyTime + (fun r : (((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool))) × List Bool => + r.1.2.1.1.length == msgLen r.1.1.1.1) encR encBool := by + polytime + have hlenEq : ComputableTidilyInPolyTime + (fun p : List Bool × ℕ => p.1.length == p.2) + (encPair encBits encUnary) encBool := by + polytime + have hc2 : ComputableTidilyInPolyTime + (fun r : (((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool))) × List Bool => + (unframe r.1.2.1.2).length == r.1.1.1.1) encR encBool := + hlenEq.comp ((hunframe.comp (by polytime)).prod (by polytime)) + have hc3 : ComputableTidilyInPolyTime + (fun r : (((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool))) × List Bool => + !r.1.2.2.contains r.1.2.1) encR encBool := by + polytime + have hbitsEq : ComputableTidilyInPolyTime + (fun p : List Bool × List Bool => p.1 == p.2) + (encPair encBits encBits) encBool := by + polytime + have hc4 : ComputableTidilyInPolyTime + (fun r : (((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool))) × List Bool => + expectedFullTag r == r.1.2.1.2) encR encBool := + hbitsEq.comp (hexpected.prod (by polytime)) + have hand : ComputableTidilyInPolyTime + (fun p : Bool × Bool => p.1 && p.2) (encPair encBool encBool) encBool := + ComputableInPolyTime.bool_and.tidy + have hpost : ComputableTidilyInPolyTime + (fun r : (((ℕ × List Bool) × List Bool) × + ((List Bool × List Bool) × List (List Bool × List Bool))) × List Bool => + (r.1.2.1.1.length == msgLen r.1.1.1.1) && ((unframe r.1.2.1.2).length == r.1.1.1.1) && + !r.1.2.2.contains r.1.2.1 && + (expectedFullTag r == r.1.2.1.2)) encR encBool := + hand.comp ((hand.comp ((hand.comp (hc1.prod hc2)).prod hc3)).prod hc4) + exact (IsOraclePPTOn.query_take () (hunframe.comp (by polytime)) (by polytime)).map_with hpost + +/-- `prfRandomNonceToPrfDistinguisher` is uniformly strict oracle-PPT (`IsOraclePPT encBool`) +whenever `msgLen`, `seed`, `hash`, and `adversary` are uniformly polynomial-time / strict PPT. -/ +theorem isOraclePPT_prfRandomNonceToPrfDistinguisher + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} {adversary : Forger} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hadversary : IsOraclePPT (encPair encBits encBits) adversary) : + IsOraclePPT encBool (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) := by + have hhandler := isOraclePPTOn_cwRandomNonceLogHandler hmsgLen hhash + have hrun : IsOraclePPTOn + (encPair (encPair encUnary encBits) encBits) + (encPair (encPair encBits encBits) (encList (encPair encBits encBits))) + (fun caller : (ℕ × List Bool) × List Bool => + (OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (cwRandomNonceLogHandler msgLen hash caller.1.1 caller.2)) + (adversary caller.1.1 [])).run []) := by + apply hadversary.run_interpret_preprocess_open + (prepare := fun caller : (ℕ × List Bool) × List Bool => (caller.1.1, ([] : List Bool))) + (initial := fun _ => ([] : List (List Bool × List Bool))) + (resources := fun caller query => 6 * caller.1.1 + 4 * query.length + 10) + (by fun_prop) hhandler (by fun_prop) + (fun _ _ => True) (fun _ => trivial) (by fun_prop) + intro caller request queriedPairs _ result hresult + dsimp only [cwRandomNonceLogHandler] at hresult + by_cases hcond : (request.2.length == msgLen caller.1.1) = true + · simp only [hcond, ↓reduceIte, OracleComp.mem_supportWith_bind_iff, + OracleComp.mem_supportWith_map_iff] at hresult + rcases hresult with ⟨nonce, hnonce, pad, -, rfl⟩ + change nonce ∈ OracleComp.support + (ProbOracleComp.sample (BitString.sampleList caller.1.1)) at hnonce + rw [ProbOracleComp.support_sample, BitString.eval_sampleList] at hnonce + have hnonceLen : nonce.length = caller.1.1 := + BitString.length_of_mem_support_uniformList hnonce + refine ⟨trivial, ?_, ?_⟩ + · simp only [length_encPair, encBits_apply, hnonceLen, BitString.length_listXor] + lia + · simp only [encList_cons, List.length_append, length_frame, length_encPair, encBits_apply, + hnonceLen, BitString.length_listXor] + lia + · have hcond' : (request.2.length == msgLen caller.1.1) = false := + Bool.eq_false_iff.mpr hcond + simp only [hcond', Bool.false_eq_true, ↓reduceIte, OracleComp.supportWith_pure, + Set.mem_singleton_iff] at hresult + subst hresult + refine ⟨trivial, ?_, ?_⟩ + · simp + · simp only [encList_cons, List.length_append, length_frame, length_encPair, encBits_apply, + List.length_nil] + lia + have hk : IsOraclePPTOn (Operation := Unit) (encPair encUnary encBits) encBits + (fun caller : ℕ × List Bool => ProbOracleComp.sample (seed caller.1)) := + (hseed.preprocess (ComputableInPolyTime.fst _ _)).isOraclePPTOn + have hcheck := isOraclePPTOn_cwRandomNonceCheck hmsgLen hhash + exact (hk.bind_with (hrun.bind_with hcheck)).isOraclePPT + +/-- **Real-game simulation for `prfRandomNonceToPrfDistinguisher`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): running `prfRandomNonceToPrfDistinguisher` in +`prfRealGame family` at security parameter `n` has the exact same acceptance distribution as the +computational `MACScheme.sufCmaGame` of `carterWegmanRandomMAC`. -/ +theorem eval_prfRealGame_prfRandomNonceToPrfDistinguisher + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) + (adversary : Forger) (n : ℕ) : + ProbComp.eval (prfRealGame family + (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) = + ProbComp.eval + ((carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame + adversary n) := by + let M := carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hfamily + change ProbComp.eval + (prfRealGame family (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) = + ProbComp.eval (M.sufCmaGame adversary n) + dsimp only [prfRealGame, prfRandomNonceToPrfDistinguisher, MACScheme.sufCmaGame, M, + carterWegmanRandomMAC] + simp only [Functor.map_map, OracleComp.interpret_bind, OracleComp.interpret_map, + ProbOracleComp.interpret_sample, ProbOracleComp.interpret_query, interpret_unifFin, + ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_pure, PMF.bind_bind, PMF.pure_bind, + PMF.pure_map] + rw [PMF.bind_comm (ProbComp.eval (BitString.sampleList n)) (ProbComp.eval (seed n))] + refine PMF.bind_congr_on_support _ _ _ fun k _ => ?_ + refine PMF.bind_congr_on_support _ _ _ fun prfKey hprfKey => ?_ + rw [BitString.eval_sampleList] at hprfKey + have hprfLen : prfKey.length = n := BitString.length_of_mem_support_uniformList hprfKey + rw [interpret_deterministic_run_interpret, ProbOracleComp.eval_run_interpret, + ProbOracleComp.eval_run_interpret] + have hstep : + (fun request state => + ProbComp.eval + (OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin + (fun req => pure (prfOracle family n prfKey req.2))) + (cwRandomNonceLogHandler msgLen hash n k request state))) = + (fun request state => + ProbComp.eval + (M.signingPairOracle (encPair encBits encBits (k, prfKey)) request state)) := by + funext request state + dsimp only [cwRandomNonceLogHandler, MACScheme.signingPairOracle, M, carterWegmanRandomMAC] + simp only [encPair_apply, encBits_apply, unframe_frame_append, dropFrame_frame_append, + hprfLen] + by_cases hcond : (request.2.length == msgLen n) = true + · simp [hcond, Functor.map_map] + · have hcond' : (request.2.length == msgLen n) = false := Bool.eq_false_iff.mpr hcond + have hconst : + PMF.map (fun _ : List Bool => (([] : List Bool), (request.2, []) :: state)) + (BitString.uniformList n) = + PMF.pure (([] : List Bool), (request.2, []) :: state) := + PMF.map_const (BitString.uniformList n) (([] : List Bool), (request.2, []) :: state) + simp [hcond', hconst] + rw [hstep] + refine PMF.bind_congr_on_support _ _ _ fun out _ => ?_ + simp only [encPair_apply, encBits_apply, unframe_frame_append, dropFrame_frame_append, hprfLen] + congr 1 + cases (out.1.1.length == msgLen n) <;> cases ((unframe out.1.2).length == n) <;> + cases out.2.contains out.1 <;> rfl + +open scoped List + +/-- Decode a candidate `(msg, fullTag)` pair into a typed triple on +`BitString (msgLen n) × BitString n × BitString n`. -/ +private def toRandomBitTriple (msgLen : ℕ → ℕ) (n : ℕ) (out : List Bool × List Bool) : + (BitString (msgLen n) × BitString n) × BitString n := + ((BitString.ofList (msgLen n) out.1, BitString.ofList n (unframe out.2)), + BitString.ofList n (dropFrame out.2)) + +/-- Encode a typed `((m, x), t)` triple back to +`(List.ofFn m, encPair encBits encBits (List.ofFn x, List.ofFn t))`. -/ +private def ofRandomBitTriple {m n : ℕ} (e : (BitString m × BitString n) × BitString n) : + List Bool × List Bool := + (List.ofFn e.1.1, encPair encBits encBits (List.ofFn e.1.2, List.ofFn e.2)) + +/-- Step adapter translating word-level signing requests `request.2` into typed queries on +`BitString (msgLen n)` while maintaining the word-level pair log `queriedPairs`. -/ +private def adaptRandomNonceStep (msgLen : ℕ → ℕ) (n : ℕ) (request : Unit × List Bool) + (queriedPairs : List (List Bool × List Bool)) : + ProbOracleComp (fun _ : BitString (msgLen n) => BitString n × BitString n) + (List Bool × List (List Bool × List Bool)) := + let msg := request.2 + if msg.length == msgLen n then + (fun xt : BitString n × BitString n => + let fullTag := encPair encBits encBits (List.ofFn xt.1, List.ofFn xt.2) + (fullTag, (msg, fullTag) :: queriedPairs)) <$> + ProbOracleComp.query (BitString.ofList (msgLen n) msg) + else + pure ([], (msg, []) :: queriedPairs) + +private theorem isQueryBounded_adaptRandomNonceStep (msgLen : ℕ → ℕ) (n : ℕ) + {α : Type} {prog : WordOracleComp Unit α} {Q : ℕ} (hprog : prog.IsQueryBounded Q) + (init : List (List Bool × List Bool)) : + ((OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptRandomNonceStep msgLen n)) + prog).run init).IsQueryBounded Q := by + refine OracleComp.IsCostBounded.run_interpret (fun q s => ?_) hprog init + cases q with + | inl m => + simp only [ProbOracleComp.handler, StateT.run_lift, Sum.elim_inl] + simpa using (ProbOracleComp.IsQueryBounded.sample (ProbComp.unifFin m)).bind + fun a => .pure (a, s) 0 + | inr req => + dsimp only [ProbOracleComp.handler, StateT.run, adaptRandomNonceStep, Sum.elim_inr] + split_ifs + · rw [OracleComp.isCostBounded_map_iff] + exact ProbOracleComp.IsQueryBounded.query (BitString.ofList (msgLen n) req.2) + · exact OracleComp.IsCostBounded.pure _ 1 + +/-- Word-level acceptance check of `prfRandomNonceToPrfDistinguisher` in `prfIdealGame` against a +random function `table : BitString n → BitString n`. -/ +private def cwRandomNonceIdealCheck (msgLen : ℕ → ℕ) + (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (table : BitString n → BitString n) + (out : (List Bool × List Bool) × List (List Bool × List Bool)) : Bool := + let msg := out.1.1 + let fullTag := out.1.2 + let nonce := unframe fullTag + let pad := (randomFunctionOracle n table nonce).take n + let tag := BitString.listXor n [hash n k msg, pad] + (msg.length == msgLen n) && (nonce.length == n) && !out.2.contains out.1 && + (encPair encBits encBits (nonce, tag) == fullTag) + +private theorem cwRandomNonceIdealCheck_imp_checkRandomNonceSUF + (msgLen : ℕ → ℕ) (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (table : BitString n → BitString n) + (out : (List Bool × List Bool) × List (List Bool × List Bool)) + (tr : List ((BitString (msgLen n) × BitString n) × BitString n)) + (hsub : tr.map ofRandomBitTriple <+ out.2.reverse) + (hcheck : cwRandomNonceIdealCheck msgLen hash n k table out = true) : + checkRandomNonceSUF + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table tr (toRandomBitTriple msgLen n out.1) = true := by + dsimp only [cwRandomNonceIdealCheck] at hcheck + simp only [Bool.and_eq_true, Bool.not_eq_true', List.contains_eq_mem, decide_eq_false_iff_not, + beq_iff_eq] at hcheck + rcases hcheck with ⟨⟨⟨hmsg, hnonce⟩, hnotmem⟩, hfullTag⟩ + have hdrop : + dropFrame out.1.2 = + BitString.listXor n + [hash n k out.1.1, (randomFunctionOracle n table (unframe out.1.2)).take n] := by + have h := congrArg dropFrame hfullTag.symm + simpa only [encPair_apply, encBits_apply, dropFrame_frame_append] using h + have htag : (dropFrame out.1.2).length = n := by + rw [hdrop, BitString.length_listXor] + have hround : ofRandomBitTriple (toRandomBitTriple msgLen n out.1) = out.1 := by + dsimp only [ofRandomBitTriple, toRandomBitTriple] + rw [BitString.ofFn_ofList hmsg, BitString.ofFn_ofList hnonce, BitString.ofFn_ofList htag, + hdrop, hfullTag] + simp only [checkRandomNonceSUF, Bool.and_eq_true, Bool.not_eq_true', List.contains_eq_mem, + decide_eq_false_iff_not] + refine ⟨?_, ?_⟩ + · intro hin + have hmem : out.1 ∈ tr.map ofRandomBitTriple := by + rw [← hround] + exact List.mem_map_of_mem hin + exact hnotmem (List.mem_reverse.mp (hsub.subset hmem)) + · simp only [verify, toRandomBitTriple, BitString.ofFn_ofList hmsg, decide_eq_true_eq] + rw [hdrop] + simp only [randomFunctionOracle, hnonce, ↓reduceIte, BitString.listXor_pair, + ofList_take, BitString.ofList_ofFn] + +private theorem eval_cwRandomNonceLogHandler_randomFunctionOracle_le + (msgLen : ℕ → ℕ) (hash : ℕ → List Bool → List Bool → List Bool) + (n : ℕ) (k : List Bool) (table : BitString n → BitString n) + (prog : WordOracleComp Unit (List Bool × List Bool)) + (init : List (List Bool × List Bool)) + (tr : List ((BitString (msgLen n) × BitString n) × BitString n)) + (hsub : tr.map ofRandomBitTriple <+ init.reverse) : + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (fun request state => + ProbComp.eval + (OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin + (fun req => pure (randomFunctionOracle n table req.2))) + (cwRandomNonceLogHandler msgLen hash n k request state)))) + prog).run init).bind fun out => + PMF.pure (cwRandomNonceIdealCheck msgLen hash n k table out)) true ≤ + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + ((OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptRandomNonceStep msgLen n)) + prog).run init)).run tr).bind fun res => + PMF.pure + (checkRandomNonceSUF + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table res.2 (toRandomBitTriple msgLen n res.1.1))) true := by + induction prog using OracleComp.induction generalizing init tr with + | pure a => + simp only [OracleComp.run_interpret_pure, PMF.monad_pure_eq_pure, PMF.pure_bind] + by_cases h : cwRandomNonceIdealCheck msgLen hash n k table (a, init) = true + · rw [h, cwRandomNonceIdealCheck_imp_checkRandomNonceSUF msgLen hash n k table (a, init) tr + hsub h] + · simp [Bool.eq_false_iff.mpr h] + | query_bind q cont ih => + rw [OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + OracleComp.run_interpret_bind, OracleComp.run_interpret_query, + OracleComp.run_interpret_bind] + cases q with + | inl num => + have hsample : + (StateT.lift (ProbOracleComp.sample (ProbComp.unifFin num)) init : + ProbOracleComp (fun _ : BitString (msgLen n) => BitString n × BitString n) + (Fin (num + 1) × List (List Bool × List Bool))) = + (OracleComp.query (Sum.inl num) >>= fun i => pure (i, init)) := by + simp [StateT.lift, ProbOracleComp.sample, ProbComp.unifFin] + rw [ProbOracleComp.handler, ProbOracleComp.handler, hsample, + OracleComp.run_interpret_bind, OracleComp.run_interpret_query] + simp only [ProbOracleComp.handler, StateT.lift, OracleComp.run_interpret_pure, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, PMF.bind_bind, PMF.pure_bind] + refine bind_apply_mono_on_support (ProbComp.unifOracle num) true fun i _ => ?_ + exact ih i init tr hsub + | inr req => + dsimp only [ProbOracleComp.handler, cwRandomNonceLogHandler, adaptRandomNonceStep] + let msg := req.2 + change (((OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin + (fun r => pure (randomFunctionOracle n table r.2))) + (if (msg.length == msgLen n) = true then do + let nonce ← ProbOracleComp.sample (BitString.sampleList n) + (fun pad => + let tag := BitString.listXor n [hash n k msg, pad] + let fullTag := encPair encBits encBits (nonce, tag) + (fullTag, (msg, fullTag) :: init)) <$> + (List.take n <$> ProbOracleComp.query ((), nonce)) + else + pure ([], (msg, []) :: init))).eval >>= fun x => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (fun request state => + ProbComp.eval + (OracleComp.interpret + (ProbOracleComp.handler ProbComp.unifFin + (fun req => pure (randomFunctionOracle n table req.2))) + (cwRandomNonceLogHandler msgLen hash n k request state)))) + (cont x.1)).run x.2)).bind + fun out => PMF.pure (cwRandomNonceIdealCheck msgLen hash n k table out)) true ≤ + (((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + (if (msg.length == msgLen n) = true then + (fun xt : BitString n × BitString n => + let fullTag := encPair encBits encBits (List.ofFn xt.1, List.ofFn xt.2) + (fullTag, (msg, fullTag) :: init)) <$> + ProbOracleComp.query (BitString.ofList (msgLen n) msg) + else + pure ([], (msg, []) :: init))).run tr >>= fun x => + (OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + ((OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptRandomNonceStep msgLen n)) + (cont x.1.1)).run x.1.2)).run x.2).bind + fun res => + PMF.pure + (checkRandomNonceSUF + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table res.2 (toRandomBitTriple msgLen n res.1.1))) true + by_cases hcond : (msg.length == msgLen n) = true + · simp only [hcond, ↓reduceIte] + rw [OracleComp.run_interpret_map] + have hq_rhs : + (OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table)) + (ProbOracleComp.query (BitString.ofList (msgLen n) msg))).run tr = + randomNonceFnHandler + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k table (BitString.ofList (msgLen n) msg) tr := + OracleComp.run_interpret_query _ (Sum.inr (BitString.ofList (msgLen n) msg)) tr + rw [hq_rhs] + simp only [Functor.map_map, OracleComp.interpret_bind, OracleComp.interpret_map, + ProbOracleComp.interpret_sample, ProbOracleComp.interpret_query, interpret_unifFin, + ProbComp.eval_bind, ProbComp.eval_map, ProbComp.eval_pure, BitString.eval_sampleList, + randomNonceFnHandler, PMF.monad_bind_eq_bind, PMF.monad_map_eq_map, + PMF.monad_pure_eq_pure, PMF.map_bind, PMF.pure_map, PMF.bind_bind, PMF.pure_bind] + rw [BitString.uniformList, PMF.bind_map] + refine bind_apply_mono_on_support (PMF.uniformOfFintype (BitString n)) true fun x _ => ?_ + simp only [Function.comp_def] + simp only [beq_iff_eq] at hcond + let t := sign + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) + k (table x) (BitString.ofList (msgLen n) msg) + have htag : List.ofFn t = + BitString.listXor n + [hash n k msg, (randomFunctionOracle n table (List.ofFn x)).take n] := by + simp only [t, sign, BitString.ofFn_ofList hcond, randomFunctionOracle, List.length_ofFn, + ↓reduceIte, BitString.listXor_pair, ofList_take, BitString.ofList_ofFn] + rw [← htag] + let fullTag := encPair encBits encBits (List.ofFn x, List.ofFn t) + have hsub' : + (tr ++ [((BitString.ofList (msgLen n) msg, x), t)]).map ofRandomBitTriple <+ + ((msg, fullTag) :: init).reverse := by + rw [List.map_append, List.map_singleton, List.reverse_cons] + have he : ofRandomBitTriple ((BitString.ofList (msgLen n) msg, x), t) = + (msg, fullTag) := by + simp [ofRandomBitTriple, fullTag, BitString.ofFn_ofList hcond] + rw [he] + exact hsub.append (List.Sublist.refl _) + exact ih fullTag ((msg, fullTag) :: init) + (tr ++ [((BitString.ofList (msgLen n) msg, x), t)]) hsub' + · have hcond' : (msg.length == msgLen n) = false := Bool.eq_false_iff.mpr hcond + simp only [hcond', Bool.false_eq_true, ↓reduceIte, OracleComp.interpret_pure, + ProbComp.eval_pure, StateT.run_pure, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure, + PMF.pure_bind] + have hsub' : tr.map ofRandomBitTriple <+ ((msg, []) :: init).reverse := by + rw [List.reverse_cons] + exact hsub.trans (List.sublist_append_left _ _) + exact ih [] ((msg, []) :: init) tr hsub' + +/-- **Ideal-game bound for `prfRandomNonceToPrfDistinguisher`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): under +`IsDeltaUniversalHash (ProbComp.eval (seed n)) ... ε`, if `adversary n []` makes at most `Q` signing +queries, the ideal-game acceptance probability of +`prfRandomNonceToPrfDistinguisher msgLen seed hash adversary` at parameter `n` is at most +`(Q : ℝ≥0∞) ^ 2 / (2 * (2 : ℝ≥0∞) ^ n) + ((2 : ℝ≥0∞) ^ n)⁻¹ + ε`. -/ +theorem eval_prfIdealGame_prfRandomNonceToPrfDistinguisher_le + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} {n Q : ℕ} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) + {adversary : Forger} (hq : (adversary n []).IsQueryBounded Q) : + ProbComp.eval + (prfIdealGame (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) true ≤ + (Q : ℝ≥0∞) ^ 2 / (2 * (2 : ℝ≥0∞) ^ n) + ((2 : ℝ≥0∞) ^ n)⁻¹ + ε := by + let hashBit : List Bool → BitString (msgLen n) → BitString n := + fun k m => BitString.ofList n (hash n k (List.ofFn m)) + let adaptProg : ProbOracleComp (fun _ : BitString (msgLen n) => BitString n × BitString n) + ((List Bool × List Bool) × List (List Bool × List Bool)) := + (OracleComp.interpret + (ProbOracleComp.handler + (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) + (adaptRandomNonceStep msgLen n)) + (adversary n [])).run [] + have hle : + ProbComp.eval + (prfIdealGame (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) true ≤ + ((ProbComp.eval (seed n)).bind fun k => + (PMF.uniformOfFintype (BitString n → BitString n)).bind fun table => + ((OracleComp.interpret + (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (randomNonceFnHandler hashBit k table)) + adaptProg).run []).bind fun res => + PMF.pure + (checkRandomNonceSUF hashBit k table res.2 + (toRandomBitTriple msgLen n res.1.1))) true := by + simp only [prfIdealGame, prfRandomNonceToPrfDistinguisher, Functor.map_map, + OracleComp.interpret_bind, OracleComp.interpret_map, ProbOracleComp.interpret_sample, + ProbOracleComp.interpret_query, interpret_unifFin, ProbComp.eval_bind, ProbComp.eval_map, + ProbComp.eval_pure, ProbComp.eval_uniform, PMF.pure_map] + rw [PMF.bind_comm (PMF.uniformOfFintype (BitString n → BitString n)) (ProbComp.eval (seed n))] + refine bind_apply_mono_on_support (ProbComp.eval (seed n)) true fun k _ => ?_ + refine bind_apply_mono_on_support (PMF.uniformOfFintype (BitString n → BitString n)) true + fun table _ => ?_ + rw [interpret_deterministic_run_interpret, ProbOracleComp.eval_run_interpret] + exact eval_cwRandomNonceLogHandler_randomFunctionOracle_le msgLen hash n k table + (adversary n []) [] [] (List.Sublist.refl []) + refine hle.trans ?_ + have hq_adapt : adaptProg.IsQueryBounded Q := + isQueryBounded_adaptRandomNonceStep msgLen n hq [] + simpa only [BitString.card, Nat.cast_pow, Nat.cast_ofNat] using + seed_uniform_probOracleComp_checkRandomNonceSUF_le hh hq_adapt + (fun out => toRandomBitTriple msgLen n out.1) + +/-- **Quantitative SUF-CMA bound for `carterWegmanRandomMAC`** ([BonehShoup2023], Section 7.4, +Theorem 7.9, p. 270): at security parameter `n`, the SUF-CMA forgery probability of any `Q`-query +`Forger` against `carterWegmanRandomMAC` is at most +`(Q : ℝ) ^ 2 / (2 * (2 : ℝ) ^ n) + ((2 : ℝ) ^ n)⁻¹ + ε.toReal` plus the PRF distinguishing +advantage of `prfRandomNonceToPrfDistinguisher msgLen seed hash adversary`. -/ +theorem sufCmaGame_carterWegmanRandomMAC_toReal_le + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) + {n Q : ℕ} {ε : ℝ≥0∞} + (hh : IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) + (hε : ε ≠ ⊤) {adversary : Forger} (hq : (adversary n []).IsQueryBounded Q) : + (ProbComp.eval + ((carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame + adversary n) true).toReal ≤ + (Q : ℝ) ^ 2 / (2 * (2 : ℝ) ^ n) + ((2 : ℝ) ^ n)⁻¹ + ε.toReal + + (Game.advantage + (ProbComp.eval + (prfRealGame family + (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n)) + (ProbComp.eval + (prfIdealGame + (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n)) : ℝ) := by + rw [← eval_prfRealGame_prfRandomNonceToPrfDistinguisher hmsgLen hseed hhash hfamily adversary n] + have hcol_ne_top : (Q : ℝ≥0∞) ^ 2 / (2 * (2 : ℝ≥0∞) ^ n) ≠ ⊤ := + ENNReal.div_ne_top (ENNReal.pow_ne_top (ENNReal.natCast_ne_top Q)) + (mul_ne_zero (by norm_num) (pow_ne_zero n (by norm_num))) + have hinv_ne_top : ((2 : ℝ≥0∞) ^ n)⁻¹ ≠ ⊤ := by simp + have hideal : + (ProbComp.eval + (prfIdealGame + (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) true).toReal ≤ + (Q : ℝ) ^ 2 / (2 * (2 : ℝ) ^ n) + ((2 : ℝ) ^ n)⁻¹ + ε.toReal := by + have htr := ENNReal.toReal_mono + (ENNReal.add_ne_top.mpr ⟨ENNReal.add_ne_top.mpr ⟨hcol_ne_top, hinv_ne_top⟩, hε⟩) + (eval_prfIdealGame_prfRandomNonceToPrfDistinguisher_le hh hq) + simpa only [ENNReal.toReal_add (ENNReal.add_ne_top.mpr ⟨hcol_ne_top, hinv_ne_top⟩) hε, + ENNReal.toReal_add hcol_ne_top hinv_ne_top, ENNReal.toReal_div, ENNReal.toReal_pow, + ENNReal.toReal_natCast, ENNReal.toReal_mul, ENNReal.toReal_ofNat, + ENNReal.toReal_inv] using htr + rw [Game.coe_advantage, Game.coe_succProbability, Game.coe_succProbability] + linarith [le_abs_self + ((ProbComp.eval + (prfRealGame family + (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) true).toReal - + (ProbComp.eval + (prfIdealGame + (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n) true).toReal)] + +/-- **Asymptotic `MACScheme.SUFCMA` security of `carterWegmanRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): if `family` is a `PseudorandomFunction` and +`(seed n, hash n)` is an `(ε n)`-almost-Δ-universal hash family on `BitString (msgLen n)` into +`BitString n` with `Negligible ε`, then `carterWegmanRandomMAC` satisfies `MACScheme.SUFCMA`. -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.sufCma_carterWegmanRandomMAC + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + {ε : ℕ → ℝ≥0} + (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) (ε n)) + (hε : Negligible ε) : + (carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hprf.polyTime).SUFCMA := by + refine MACScheme.SUFCMA.of_negligible fun adversary hadversary => ?_ + obtain ⟨c, d, hbound⟩ := hadversary.query_bounds + let Q (n : ℕ) : ℕ := c * (n + 2) ^ d + have hQ : PolynomiallyBounded Q := by + refine polynomiallyBounded_iff_le.2 ⟨c * 2 ^ d, d, fun n => ?_⟩ + have hle : n + 2 ≤ 2 * (n + 1) := by omega + calc c * (n + 2) ^ d + ≤ c * (2 * (n + 1)) ^ d := Nat.mul_le_mul_left c (Nat.pow_le_pow_left hle d) + _ = c * 2 ^ d * (n + 1) ^ d := by rw [Nat.mul_pow, Nat.mul_assoc] + have hgeom : Negligible (fun n => ((2 : ℝ≥0) ^ n)⁻¹) := by + simpa only [inv_pow] using negligible_geometric (ratio := 2⁻¹) (by norm_num) + have hcol : Negligible (fun n => (Q n : ℝ≥0) ^ 2 / (2 * (2 : ℝ≥0) ^ n)) := by + refine negligible_of_le (hgeom.polynomiallyBounded_mul (hQ.pow 2)) fun n => ?_ + rw [div_eq_mul_inv, mul_inv, Nat.cast_pow] + exact mul_le_mul_of_nonneg_left + (mul_le_of_le_one_left zero_le (by norm_num : (2⁻¹ : ℝ≥0) ≤ 1)) zero_le + have hdist := hprf.secure (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) + (isOraclePPT_prfRandomNonceToPrfDistinguisher hmsgLen hseed hhash hadversary) + refine negligible_of_le (((hcol.add hgeom).add hε).add hdist) fun n => ?_ + have hq_n : (adversary n []).IsQueryBounded (Q n) := by + simpa [Q] using (hbound n []).1 + rw [← NNReal.coe_le_coe, Game.coe_succProbability] + simp only [Pi.add_apply, NNReal.coe_add, NNReal.coe_div, NNReal.coe_pow, NNReal.coe_natCast, + NNReal.coe_mul, NNReal.coe_ofNat, NNReal.coe_inv] + simpa only [ENNReal.coe_toReal] using + sufCmaGame_carterWegmanRandomMAC_toReal_le hmsgLen hseed hhash hprf.polyTime + (hh n) ENNReal.coe_ne_top hq_n + +/-- **Asymptotic `MACScheme.EUFCMA` security of `carterWegmanRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270). -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.eufCma_carterWegmanRandomMAC + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + {ε : ℕ → ℝ≥0} + (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) (ε n)) + (hε : Negligible ε) : + (carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hprf.polyTime).EUFCMA := + (hprf.sufCma_carterWegmanRandomMAC hmsgLen hseed hhash hh hε).eufCma + +/-- **Asymptotic `MACScheme.OneTimeEUFCMA` security of `carterWegmanRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270). -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_carterWegmanRandomMAC + {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} + {hash : ℕ → List Bool → List Bool → List Bool} + {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hseed : IsPPTOn encUnary encBits seed) + (hhash : ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => hash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits) + {ε : ℕ → ℝ≥0} + (hh : ∀ n, IsDeltaUniversalHash (ProbComp.eval (seed n)) + (fun k (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) (ε n)) + (hε : Negligible ε) : + (carterWegmanRandomMAC msgLen seed hash family + hmsgLen hseed hhash hprf.polyTime).OneTimeEUFCMA := + (hprf.sufCma_carterWegmanRandomMAC hmsgLen hseed hhash hh hε).oneTimeEUFCMA + end Randomized /-! ### Concrete Carter–Wegman instantiations -/ @@ -3429,6 +5754,205 @@ theorem nonceStrongGame_of_isPairwiseIndependentHash_le {K M N Y : Type} [Fintyp nonceStrongGame (PMF.uniformOfFintype K) hash forger true ≤ (Fintype.card Y : ℝ≥0∞)⁻¹ := by simpa only [max_self] using nonceStrongGame_le_max hh.isDeltaUniversalHash forger +/-- Sampling an `(n * msgLen n)`-bit Boolean-matrix seed is uniformly strict PPT whenever `msgLen` +is computable in polynomial time. -/ +theorem isPPTOn_linearHashSeed {msgLen : ℕ → ℕ} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) : + IsPPTOn encUnary encBits (fun n => BitString.sampleList (n * msgLen n)) := by + have hmsgLen_tidy := hmsgLen.tidy + exact ComputableInPolyTime.sampleList (by polytime) + +/-- Uncurried `BitString.LinearHash.wordHash` is computable in plain polynomial time. -/ +theorem computableInPolyTime_linearHashWordHash : + ComputableInPolyTime + (fun p : ℕ × List Bool × List Bool => BitString.LinearHash.wordHash p.1 p.2.1 p.2.2) + (encPair encUnary (encPair encBits encBits)) encBits := by + polytime + +/-- Under a uniform `(n * msgLen n)`-bit seed `BitString.sampleList (n * msgLen n)`, the executable +Boolean-matrix hash `BitString.LinearHash.wordHash n` on `BitString (msgLen n)` into `BitString n` +is `(2 ^ n)⁻¹`-almost-Δ-universal (`IsDeltaUniversalHash`). -/ +theorem isDeltaUniversalHash_linearHashWordHash (msgLen : ℕ → ℕ) (n : ℕ) : + IsDeltaUniversalHash (ProbComp.eval (BitString.sampleList (n * msgLen n))) + (fun k (m : BitString (msgLen n)) => + BitString.ofList n (BitString.LinearHash.wordHash n k (List.ofFn m))) + ((2 : ℝ≥0∞) ^ n)⁻¹ := by + let prepare (k : List Bool) : Fin n → BitString (msgLen n) := + BitString.block (BitString.ofList (n * msgLen n) k) + have hfn : + (fun k (m : BitString (msgLen n)) => + BitString.ofList n (BitString.LinearHash.wordHash n k (List.ofFn m))) = + (fun k (m : BitString (msgLen n)) => BitString.LinearHash.hash (prepare k) m) := by + funext k m + rw [BitString.LinearHash.wordHash_eq_ofFn, BitString.ofList_ofFn] + have hmap : + (ProbComp.eval (BitString.sampleList (n * msgLen n))).map prepare = + PMF.uniformOfFintype (Fin n → BitString (msgLen n)) := by + rw [BitString.eval_sampleList, BitString.uniformList, PMF.map_comp] + have hcomp : + prepare ∘ List.ofFn = + (BitString.blocksEquiv (m := n) (k := msgLen n) : + BitString (n * msgLen n) ≃ (Fin n → BitString (msgLen n))) := by + funext s + simp [prepare, BitString.ofList_ofFn, BitString.blocksEquiv_apply] + rw [hcomp, PMF.uniformOfFintype_map_equiv] + rw [hfn] + refine IsDeltaUniversalHash.precompose_seed + (ProbComp.eval (BitString.sampleList (n * msgLen n))) prepare ?_ + rw [hmap] + simpa only [BitString.card, Nat.cast_pow, Nat.cast_ofNat] using + BitString.LinearHash.isDeltaUniversalHash (msgLen n) n + +/-- **Concrete computational nonce-based Carter–Wegman MAC (`NonceMACScheme`) from Boolean-matrix +linear hashing (`BitString.LinearHash.wordHash`) and a PRF family `family`** +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274). -/ +noncomputable def linearHashNonceMAC (msgLen : ℕ → ℕ) + (family : List Bool → List Bool → List Bool) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) : NonceMACScheme := + carterWegmanNonceMAC msgLen (fun n => BitString.sampleList (n * msgLen n)) + BitString.LinearHash.wordHash family hmsgLen (isPPTOn_linearHashSeed hmsgLen) + computableInPolyTime_linearHashWordHash hfamily + +/-- **Quantitative SUF-CMA bound for `linearHashNonceMAC`** +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274): at security parameter `n`, the SUF-CMA +forgery probability of any `NonceMACForger` against `linearHashNonceMAC` is at most +`2 * (2 ^ n)⁻¹` plus the PRF distinguishing advantage of `prfNonceToPrfDistinguisher`. -/ +theorem sufCmaGame_linearHashNonceMAC_toReal_le + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) + (n : ℕ) (adversary : NonceMACForger) : + (ProbComp.eval + ((linearHashNonceMAC msgLen family hmsgLen hfamily).sufCmaGame adversary n) true).toReal ≤ + ((2 : ℝ) ^ n)⁻¹ + ((2 : ℝ) ^ n)⁻¹ + + (Game.advantage + (ProbComp.eval + (prfRealGame family + (prfNonceToPrfDistinguisher msgLen (fun k => BitString.sampleList (k * msgLen k)) + BitString.LinearHash.wordHash adversary) n)) + (ProbComp.eval + (prfIdealGame + (prfNonceToPrfDistinguisher msgLen (fun k => BitString.sampleList (k * msgLen k)) + BitString.LinearHash.wordHash adversary) n)) : ℝ) := by + have h := sufCmaGame_carterWegmanNonceMAC_toReal_le hmsgLen (isPPTOn_linearHashSeed hmsgLen) + computableInPolyTime_linearHashWordHash hfamily + (isDeltaUniversalHash_linearHashWordHash msgLen n) (by simp) adversary + simpa only [linearHashNonceMAC, ENNReal.toReal_inv, ENNReal.toReal_pow, + ENNReal.toReal_ofNat] using h + +/-- **Asymptotic `NonceMACScheme.SUFCMA` security of `linearHashNonceMAC`** +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274): for any `PseudorandomFunction family` and +polynomial-time message-length schedule `msgLen`, `linearHashNonceMAC` satisfies +`NonceMACScheme.SUFCMA`. -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.sufCma_linearHashNonceMAC + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) : + (linearHashNonceMAC msgLen family hmsgLen hprf.polyTime).SUFCMA := by + have hgeom : Negligible (fun n => ((2 : ℝ≥0) ^ n)⁻¹) := by + simpa only [inv_pow] using negligible_geometric (ratio := 2⁻¹) (by norm_num) + exact hprf.sufCma_carterWegmanNonceMAC hmsgLen (isPPTOn_linearHashSeed hmsgLen) + computableInPolyTime_linearHashWordHash + (fun n => by + simpa only [ENNReal.coe_inv (pow_ne_zero n two_ne_zero), ENNReal.coe_pow, + ENNReal.coe_ofNat] using isDeltaUniversalHash_linearHashWordHash msgLen n) + hgeom + +/-- **Asymptotic `NonceMACScheme.EUFCMA` security of `linearHashNonceMAC`** +([BonehShoup2023], Section 7.5.1, Theorem 7.10, p. 274). -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.eufCma_linearHashNonceMAC + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) : + (linearHashNonceMAC msgLen family hmsgLen hprf.polyTime).EUFCMA := + (hprf.sufCma_linearHashNonceMAC hmsgLen).eufCma + +/-- **Concrete computational randomized Carter–Wegman MAC (`MACScheme`) from Boolean-matrix linear +hashing (`BitString.LinearHash.wordHash`) and a PRF family `family`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270). -/ +noncomputable def linearHashRandomMAC (msgLen : ℕ → ℕ) + (family : List Bool → List Bool → List Bool) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) : MACScheme := + carterWegmanRandomMAC msgLen (fun n => BitString.sampleList (n * msgLen n)) + BitString.LinearHash.wordHash family hmsgLen (isPPTOn_linearHashSeed hmsgLen) + computableInPolyTime_linearHashWordHash hfamily + +/-- **Quantitative SUF-CMA bound for `linearHashRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): at security parameter `n`, the SUF-CMA +forgery probability of any `Q`-query `Forger` against `linearHashRandomMAC` is at most +`(Q : ℝ) ^ 2 / (2 * (2 : ℝ) ^ n) + ((2 : ℝ) ^ n)⁻¹ + ((2 : ℝ) ^ n)⁻¹` plus the PRF distinguishing +advantage of `prfRandomNonceToPrfDistinguisher`. -/ +theorem sufCmaGame_linearHashRandomMAC_toReal_le + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) + (hfamily : ComputableInPolyTime + (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) + {n Q : ℕ} {adversary : Forger} (hq : (adversary n []).IsQueryBounded Q) : + (ProbComp.eval + ((linearHashRandomMAC msgLen family hmsgLen hfamily).sufCmaGame adversary n) true).toReal ≤ + (Q : ℝ) ^ 2 / (2 * (2 : ℝ) ^ n) + ((2 : ℝ) ^ n)⁻¹ + ((2 : ℝ) ^ n)⁻¹ + + (Game.advantage + (ProbComp.eval + (prfRealGame family + (prfRandomNonceToPrfDistinguisher msgLen + (fun k => BitString.sampleList (k * msgLen k)) + BitString.LinearHash.wordHash adversary) n)) + (ProbComp.eval + (prfIdealGame + (prfRandomNonceToPrfDistinguisher msgLen + (fun k => BitString.sampleList (k * msgLen k)) + BitString.LinearHash.wordHash adversary) n)) : ℝ) := by + dsimp only [linearHashRandomMAC] + have h := sufCmaGame_carterWegmanRandomMAC_toReal_le hmsgLen (isPPTOn_linearHashSeed hmsgLen) + computableInPolyTime_linearHashWordHash hfamily + (isDeltaUniversalHash_linearHashWordHash msgLen n) (by simp) hq + simpa only [ENNReal.toReal_inv, ENNReal.toReal_pow, ENNReal.toReal_ofNat] using h + +/-- **Asymptotic `MACScheme.SUFCMA` security of `linearHashRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270): for any `PseudorandomFunction family` and +polynomial-time message-length schedule `msgLen`, `linearHashRandomMAC` satisfies +`MACScheme.SUFCMA`. -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.sufCma_linearHashRandomMAC + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) : + (linearHashRandomMAC msgLen family hmsgLen hprf.polyTime).SUFCMA := by + have hgeom : Negligible (fun n => ((2 : ℝ≥0) ^ n)⁻¹) := by + simpa only [inv_pow] using negligible_geometric (ratio := 2⁻¹) (by norm_num) + exact hprf.sufCma_carterWegmanRandomMAC hmsgLen (isPPTOn_linearHashSeed hmsgLen) + computableInPolyTime_linearHashWordHash + (fun n => by + simpa only [ENNReal.coe_inv (pow_ne_zero n two_ne_zero), ENNReal.coe_pow, + ENNReal.coe_ofNat] using isDeltaUniversalHash_linearHashWordHash msgLen n) + hgeom + +/-- **Asymptotic `MACScheme.EUFCMA` security of `linearHashRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270). -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.eufCma_linearHashRandomMAC + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) : + (linearHashRandomMAC msgLen family hmsgLen hprf.polyTime).EUFCMA := + (hprf.sufCma_linearHashRandomMAC hmsgLen).eufCma + +/-- **Asymptotic `MACScheme.OneTimeEUFCMA` security of `linearHashRandomMAC`** +([BonehShoup2023], Section 7.4, Theorem 7.9, p. 270). -/ +theorem _root_.Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_linearHashRandomMAC + {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} + (hprf : PseudorandomFunction family) + (hmsgLen : ComputableInPolyTime msgLen encUnary encUnary) : + (linearHashRandomMAC msgLen family hmsgLen hprf.polyTime).OneTimeEUFCMA := + (hprf.sufCma_linearHashRandomMAC hmsgLen).oneTimeEUFCMA + end Instantiations end Cslib.Crypto.Protocols.CarterWegman diff --git a/ComplexityTests/Crypto/CarterWegman.lean b/ComplexityTests/Crypto/CarterWegman.lean index ebeac9ca06..e180bd6e40 100644 --- a/ComplexityTests/Crypto/CarterWegman.lean +++ b/ComplexityTests/Crypto/CarterWegman.lean @@ -13,14 +13,15 @@ import Mathlib.Algebra.Field.ZMod # Tests for Carter–Wegman MACs from Δ-universal hashing Checks concrete tag generation and verification for `xpolyHash` over `ZMod 7` and Boolean-matrix -linear hashing over `BitString 2`, instantiates `OneTimeForger` and a two-query adaptive -`CounterForger`, and exercises the one-time, multi-query counter, and pseudorandom-pad security -bounds of `Complexity.Crypto.Protocols.MAC.CarterWegman`. +linear hashing over `BitString 2`, instantiates `OneTimeForger`, `CounterForger`, `NonceForger`, +`RandomNonceForger`, `NonceMACForger`, and `Forger` on multi-query adaptive programs, and exercises +the one-time, multi-query counter, nonce-based, randomized, and computational (`NonceMACScheme` and +`MACScheme`) security bounds of `Complexity.Crypto.Protocols.MAC.CarterWegman`. -/ namespace ComplexityTests.Crypto.CarterWegman -open Cslib Cslib.Probability Cslib.Crypto Cslib.Crypto.Protocols.CarterWegman +open Cslib Cslib.Probability Cslib.Crypto Cslib.Crypto.Protocols.CarterWegman Turing.MultiTapeTM open scoped ENNReal instance : Fact (Nat.Prime 7) := ⟨by decide⟩ @@ -423,4 +424,187 @@ example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFun · rw [eval_prfIdealGame_prfPadDistinguisher] simp +/-! ### Computational `NonceMACScheme` and `MACScheme` Carter–Wegman tests -/ + +/-- Identity schedule `id : ℕ → ℕ` is computable in plain polynomial time in unary. -/ +theorem computableInPolyTime_id : ComputableInPolyTime (id : ℕ → ℕ) encUnary encUnary := by + polytime + +/-- Two-query adaptive `NonceMACForger` that queries `0^n` at nonce `0^n` (receiving `t₀`), +then queries `1^n` at nonce `true :: 0^(n-1)` (receiving `t₁`), and outputs a candidate forgery +`((0^n, true :: 0^(n-1)), BitString.listXor n [t₀, t₁])`. -/ +def twoQueryNonceMACForger : NonceMACForger := + fun n _ => do + let t₀ ← List.take n <$> + ProbOracleComp.query + ((), encPair encBits encBits (List.replicate n false, List.replicate n false)) + let t₁ ← List.take n <$> + ProbOracleComp.query + ((), encPair encBits encBits + (List.replicate n true, true :: List.replicate (n - 1) false)) + return ((List.replicate n false, true :: List.replicate (n - 1) false), + BitString.listXor n [t₀, t₁]) + +/-- `twoQueryNonceMACForger` is uniformly strict oracle-PPT. -/ +theorem isOraclePPT_twoQueryNonceMACForger : + IsOraclePPT (encPair (encPair encBits encBits) encBits) twoQueryNonceMACForger := by + have hq0 : IsOraclePPTOn (encPair encUnary encBits) encBits + (fun p : ℕ × List Bool => + List.take p.1 <$> + ProbOracleComp.query + ((), encPair encBits encBits (List.replicate p.1 false, List.replicate p.1 false))) := + IsOraclePPTOn.query_take () (by polytime) (by polytime) + have hq1 : IsOraclePPTOn (encPair (encPair encUnary encBits) encBits) encBits + (fun q : (ℕ × List Bool) × List Bool => + List.take q.1.1 <$> + ProbOracleComp.query + ((), encPair encBits encBits + (List.replicate q.1.1 true, true :: List.replicate (q.1.1 - 1) false))) := + IsOraclePPTOn.query_take () (by polytime) (by polytime) + have hstep1 := hq1.map_with + (output := encPair (encPair encBits encBits) encBits) + (f := fun (q : (ℕ × List Bool) × List Bool) t₁ => + ((List.replicate q.1.1 false, true :: List.replicate (q.1.1 - 1) false), + BitString.listXor q.1.1 [q.2, t₁])) + (by polytime) + unfold twoQueryNonceMACForger + exact (hq0.bind_with hstep1).isOraclePPT + +-- Concrete `IsOraclePPT` admissibility check for `prfNonceToPrfDistinguisher` on the two-query +-- adaptive `NonceMACForger` and `BitString.LinearHash.wordHash`. +example : + IsOraclePPT encBool + (prfNonceToPrfDistinguisher id + (fun n => BitString.sampleList (n * id n)) + BitString.LinearHash.wordHash + twoQueryNonceMACForger) := + isOraclePPT_prfNonceToPrfDistinguisher + computableInPolyTime_id + (isPPTOn_linearHashSeed computableInPolyTime_id) + computableInPolyTime_linearHashWordHash + isOraclePPT_twoQueryNonceMACForger + +-- End-to-end asymptotic `NonceMACScheme.SUFCMA` and `NonceMACScheme.EUFCMA` checks for +-- `linearHashNonceMAC`, plus quantitative SUF-CMA bound instantiated on `twoQueryNonceMACForger`. +example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : + (linearHashNonceMAC id family computableInPolyTime_id hprf.polyTime).SUFCMA := + hprf.sufCma_linearHashNonceMAC computableInPolyTime_id + +example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : + (linearHashNonceMAC id family computableInPolyTime_id hprf.polyTime).EUFCMA := + hprf.eufCma_linearHashNonceMAC computableInPolyTime_id + +example {family : List Bool → List Bool → List Bool} + (hfamily : ComputableInPolyTime (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) (n : ℕ) : + (ProbComp.eval + ((linearHashNonceMAC id family computableInPolyTime_id hfamily).sufCmaGame + twoQueryNonceMACForger n) true).toReal ≤ + ((2 : ℝ) ^ n)⁻¹ + ((2 : ℝ) ^ n)⁻¹ + + (Game.advantage + (ProbComp.eval + (prfRealGame family + (prfNonceToPrfDistinguisher id (fun k => BitString.sampleList (k * id k)) + BitString.LinearHash.wordHash twoQueryNonceMACForger) n)) + (ProbComp.eval + (prfIdealGame + (prfNonceToPrfDistinguisher id (fun k => BitString.sampleList (k * id k)) + BitString.LinearHash.wordHash twoQueryNonceMACForger) n)) : ℝ) := + sufCmaGame_linearHashNonceMAC_toReal_le + computableInPolyTime_id hfamily n twoQueryNonceMACForger + +/-- Two-query adaptive `Forger` for randomized Carter–Wegman (`MACScheme`): queries `0^n` +(receiving encoded `(nonce₀, tag₀)` of length at most `2 * n + 2`), queries `1^n` (receiving +encoded `(nonce₁, tag₁)`), and outputs `(0^n, raw₁)` as its candidate forgery. -/ +def twoQueryRandomMACForger : Forger := + fun n _ => do + let _ ← List.take (2 * n + 2) <$> + ProbOracleComp.query ((), List.replicate n false) + let raw₁ ← List.take (2 * n + 2) <$> + ProbOracleComp.query ((), List.replicate n true) + return (List.replicate n false, raw₁) + +/-- `twoQueryRandomMACForger` is uniformly strict oracle-PPT. -/ +theorem isOraclePPT_twoQueryRandomMACForger : + IsOraclePPT (encPair encBits encBits) twoQueryRandomMACForger := by + have hq0 : IsOraclePPTOn (encPair encUnary encBits) encBits + (fun p : ℕ × List Bool => + List.take (2 * p.1 + 2) <$> + ProbOracleComp.query ((), List.replicate p.1 false)) := + IsOraclePPTOn.query_take () (by polytime) (by polytime) + have hq1 : IsOraclePPTOn (encPair (encPair encUnary encBits) encBits) encBits + (fun q : (ℕ × List Bool) × List Bool => + List.take (2 * q.1.1 + 2) <$> + ProbOracleComp.query ((), List.replicate q.1.1 true)) := + IsOraclePPTOn.query_take () (by polytime) (by polytime) + have hstep1 := hq1.map_with + (output := encPair encBits encBits) + (f := fun (q : (ℕ × List Bool) × List Bool) raw₁ => + (List.replicate q.1.1 false, raw₁)) + (by polytime) + unfold twoQueryRandomMACForger + exact (hq0.bind_with hstep1).isOraclePPT + +/-- `twoQueryRandomMACForger` makes at most `2` signing queries. -/ +theorem isQueryBounded_twoQueryRandomMACForger (k : ℕ) : + (twoQueryRandomMACForger k []).IsQueryBounded 2 := by + unfold twoQueryRandomMACForger + refine OracleComp.IsCostBounded.bind (n := 1) (m := 1) ?_ fun _ => ?_ + · rw [OracleComp.isCostBounded_map_iff] + exact ProbOracleComp.IsQueryBounded.query ((), List.replicate k false) + · refine OracleComp.IsCostBounded.bind (n := 1) (m := 0) ?_ fun _ => ?_ + · rw [OracleComp.isCostBounded_map_iff] + exact ProbOracleComp.IsQueryBounded.query ((), List.replicate k true) + · exact OracleComp.IsCostBounded.pure _ 0 + +-- Concrete `IsOraclePPT` admissibility check for `prfRandomNonceToPrfDistinguisher` on the +-- two-query adaptive `Forger` and `BitString.LinearHash.wordHash`. +example : + IsOraclePPT encBool + (prfRandomNonceToPrfDistinguisher id + (fun n => BitString.sampleList (n * id n)) + BitString.LinearHash.wordHash + twoQueryRandomMACForger) := + isOraclePPT_prfRandomNonceToPrfDistinguisher + computableInPolyTime_id + (isPPTOn_linearHashSeed computableInPolyTime_id) + computableInPolyTime_linearHashWordHash + isOraclePPT_twoQueryRandomMACForger + +-- End-to-end asymptotic `MACScheme.SUFCMA`, `MACScheme.EUFCMA`, and `MACScheme.OneTimeEUFCMA` +-- checks for `linearHashRandomMAC`, plus quantitative SUF-CMA bound instantiated on +-- `twoQueryRandomMACForger`. +example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : + (linearHashRandomMAC id family computableInPolyTime_id hprf.polyTime).SUFCMA := + hprf.sufCma_linearHashRandomMAC computableInPolyTime_id + +example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : + (linearHashRandomMAC id family computableInPolyTime_id hprf.polyTime).EUFCMA := + hprf.eufCma_linearHashRandomMAC computableInPolyTime_id + +example {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) : + (linearHashRandomMAC id family computableInPolyTime_id hprf.polyTime).OneTimeEUFCMA := + hprf.oneTimeEUFCMA_linearHashRandomMAC computableInPolyTime_id + +example {family : List Bool → List Bool → List Bool} + (hfamily : ComputableInPolyTime (fun p : List Bool × List Bool => family p.1 p.2) + (encPair encBits encBits) encBits) (n : ℕ) : + (ProbComp.eval + ((linearHashRandomMAC id family computableInPolyTime_id hfamily).sufCmaGame + twoQueryRandomMACForger n) true).toReal ≤ + (2 : ℝ) ^ 2 / (2 * (2 : ℝ) ^ n) + ((2 : ℝ) ^ n)⁻¹ + ((2 : ℝ) ^ n)⁻¹ + + (Game.advantage + (ProbComp.eval + (prfRealGame family + (prfRandomNonceToPrfDistinguisher id + (fun k => BitString.sampleList (k * id k)) + BitString.LinearHash.wordHash twoQueryRandomMACForger) n)) + (ProbComp.eval + (prfIdealGame + (prfRandomNonceToPrfDistinguisher id + (fun k => BitString.sampleList (k * id k)) + BitString.LinearHash.wordHash twoQueryRandomMACForger) n)) : ℝ) := + sufCmaGame_linearHashRandomMAC_toReal_le + computableInPolyTime_id hfamily (isQueryBounded_twoQueryRandomMACForger n) + end ComplexityTests.Crypto.CarterWegman diff --git a/ROADMAP.md b/ROADMAP.md index 8fe3980541..400372a03f 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -131,9 +131,7 @@ families and full-input native runtime. 2012); strict-PPT samplers for integer boxes; identification security under SIS; efficiency certificates for the simulator and extractor; full interactive-view simulation; SIS for general moduli; module SIS and module LWE toward Dilithium-style schemes, as theory. -- **Symmetric:** Carter–Wegman word-level `IsOraclePPT` PRF reduction wrappers, `MACScheme` - packaging for randomized Carter–Wegman, and a computational nonce-MAC interface ([#736]); the - Naor–Reingold PRF from DDH (efficient lazy-sampling +- **Symmetric:** the Naor–Reingold PRF from DDH (efficient lazy-sampling reduction and `PseudorandomFunction` bridge; algebraic/tree evaluation and distributional prefix-hybrid bound landed) ([#1093]). - **General:** reusable adaptive reductions, public-key encryption, universal-instance zero @@ -489,7 +487,6 @@ not planned, not as proved. [#640]: https://github.com/cslib-community/complexitylib/issues/640 [#643]: https://github.com/cslib-community/complexitylib/issues/643 [#645]: https://github.com/cslib-community/complexitylib/issues/645 -[#736]: https://github.com/cslib-community/complexitylib/issues/736 [#798]: https://github.com/cslib-community/complexitylib/issues/798 [#862]: https://github.com/cslib-community/complexitylib/issues/862 [#881]: https://github.com/cslib-community/complexitylib/issues/881 From 6425baf0d07ac262f95a52e202b33131381fef94 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Wed, 28 Oct 2026 02:48:49 +0000 Subject: [PATCH 2/2] chore(crypto): address PR #1398 review feedback - Remove vacuous `NonceMACScheme.eval_sufCmaGame_eq_eufCmaGame_of_unique_tag` and `NonceMACScheme.sufCma_iff_eufCma_of_unique_tag`, and drop redundant `NonceSUFCMA` / `NonceEUFCMA` aliases in `Complexity/Crypto/Computational/MAC.lean`. - Generalize `computableTidilyInPolyTime_contains` over the element encoding and make internal polytime/framing helpers `private` in `MAC.lean` and `CarterWegman.lean`. - Align `carterWegmanNonceMAC` citation with neighbouring Section 7.5.1 locators and add the `Cslib.Crypto.Protocols.CarterWegman.` prefix to `probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler` in the `CarterWegman.lean` module docstring. --- Complexity/Crypto/Computational/MAC.lean | 141 +++--------------- .../Crypto/Protocols/MAC/CarterWegman.lean | 54 ++++++- 2 files changed, 72 insertions(+), 123 deletions(-) diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean index c5834fa266..627bd25470 100644 --- a/Complexity/Crypto/Computational/MAC.lean +++ b/Complexity/Crypto/Computational/MAC.lean @@ -81,9 +81,9 @@ $$\Pr[\text{Forge}] \le \mathrm{Adv}_{\mathrm{PRF}}(B(\mathcal{A}), n) + 2^{-n}. * `Cslib.Crypto.NonceMACForger`, `Cslib.Crypto.NonceMACScheme`: uniform nonce-based message authentication code (`sign : Key → Msg → Nonce → ProbComp Tag`) and adaptive forger ([Boneh and Shoup, Section 7.5, Attack Game 7.4][BonehShoup2023]). -* `Cslib.Crypto.NonceMACScheme.signingPairOracle`, `sufCmaGame`, `eufCmaGame`, `SUFCMA` - (`NonceSUFCMA`), `EUFCMA` (`NonceEUFCMA`): nonce-respecting adaptive chosen-message security - experiments and predicates requiring distinct queried nonces (`(tr.map (fun e => e.1.2)).Nodup`). +* `Cslib.Crypto.NonceMACScheme.signingPairOracle`, `sufCmaGame`, `eufCmaGame`, `SUFCMA`, + `EUFCMA`: nonce-respecting adaptive chosen-message security experiments and predicates requiring + distinct queried nonces (`(tr.map (fun e => e.1.2)).Nodup`). ## Main results @@ -120,11 +120,12 @@ $$\Pr[\text{Forge}] \le \mathrm{Adv}_{\mathrm{PRF}}(B(\mathcal{A}), n) + 2^{-n}. `Cslib.Crypto.PseudorandomFunction.eufCma_prfMAC`, `Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_prfMAC`: any secure uniform `PseudorandomFunction` yields a `SUFCMA`-, `EUFCMA`-, and `OneTimeEUFCMA`-secure `MACScheme`. -* `Cslib.Crypto.NonceMACScheme.isPPTOn_sufCmaGame`, `isPPT_sufCmaGame`, `isPPTOn_eufCmaGame`, +* `Cslib.Crypto.NonceMACScheme.isPPTOn_run_signingPairOracle`, + `Cslib.Crypto.NonceMACScheme.isPPTOn_sufCmaGame`, `isPPT_sufCmaGame`, `isPPTOn_eufCmaGame`, `isPPT_eufCmaGame`, `succProbability_eufCmaGame_le_sufCmaGame`, `SUFCMA.eufCma`, - `eval_sufCmaGame_eq_freshPair_of_unique_tag`, `sufCma_iff_eufCma_of_unique_tag`: strict PPT - certificates, quantitative / asymptotic implication from `SUFCMA` to `EUFCMA`, and unique-tag - characterizations for nonce-based MACs. + `eval_sufCmaGame_eq_freshPair_of_unique_tag`: strict PPT certificates, quantitative / + asymptotic implication from `SUFCMA` to `EUFCMA`, and unique-tag pair-freshness characterization + for nonce-based MACs. ## References @@ -181,10 +182,11 @@ private theorem MACScheme.verify_polyTime_tidy (M : MACScheme) : simpa only [← computableInPolyTime_iff_computableTidilyInPolyTime] using M.verify_polyTime @[local fun_prop] -private theorem computableTidilyInPolyTime_contains {γ : Type} {encIn : γ ↪ List Bool} - {list : γ → List (List Bool)} {elem : γ → List Bool} - (hlist : ComputableTidilyInPolyTime list encIn (encList encBits)) - (helem : ComputableTidilyInPolyTime elem encIn encBits) : +private theorem computableTidilyInPolyTime_contains {γ α : Type} [BEq α] [LawfulBEq α] + {encIn : γ ↪ List Bool} {encElem : α ↪ List Bool} + {list : γ → List α} {elem : γ → α} + (hlist : ComputableTidilyInPolyTime list encIn (encList encElem)) + (helem : ComputableTidilyInPolyTime elem encIn encElem) : ComputableTidilyInPolyTime (fun a => (list a).contains (elem a)) encIn encBool := by have heq : (fun a => (list a).contains (elem a)) = (fun a => (list a).any (fun x => elem a == x)) := by @@ -193,7 +195,10 @@ private theorem computableTidilyInPolyTime_contains {γ : Type} {encIn : γ ↪ simp only [beq_iff_eq] exact ⟨fun h => ⟨elem a, h, rfl⟩, fun ⟨_, h, heq⟩ => heq ▸ h⟩ rw [heq] - exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist (by polytime) + exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist + (ComputableTidilyInPolyTime.beq (encB := encElem) + (helem.comp (ComputableTidilyInPolyTime.fst _ _)) + (ComputableTidilyInPolyTime.snd _ _)) namespace MACScheme @@ -1679,54 +1684,10 @@ structure NonceMACScheme where ∀ tag, tag ∈ (ProbComp.eval (sign sk msg nonce)).support → verify sk msg nonce tag = true -/-- Testing membership in a framed list of bit-string pairs is computable tidily in polynomial time. --/ -@[fun_prop] -theorem computableTidilyInPolyTime_contains_pair {γ : Type} {encIn : γ ↪ List Bool} - {list : γ → List (List Bool × List Bool)} - {elem : γ → List Bool × List Bool} - (hlist : ComputableTidilyInPolyTime list encIn (encList (encPair encBits encBits))) - (helem : ComputableTidilyInPolyTime elem encIn (encPair encBits encBits)) : - ComputableTidilyInPolyTime (fun a => (list a).contains (elem a)) encIn encBool := by - have heq : (fun a => (list a).contains (elem a)) = - (fun a => (list a).any (fun x => elem a == x)) := by - funext a - rw [Bool.eq_iff_iff, List.contains_iff_mem, List.any_eq_true] - simp only [beq_iff_eq] - exact ⟨fun h => ⟨elem a, h, rfl⟩, fun ⟨_, h, heq⟩ => heq ▸ h⟩ - rw [heq] - exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist - (ComputableTidilyInPolyTime.beq (encB := encPair encBits encBits) - (helem.comp (ComputableTidilyInPolyTime.fst _ _)) - (ComputableTidilyInPolyTime.snd _ _)) - -/-- Testing membership in a framed list of `((msg, nonce), tag)` triples is computable tidily in -polynomial time. -/ -@[fun_prop] -theorem computableTidilyInPolyTime_contains_triple {γ : Type} {encIn : γ ↪ List Bool} - {list : γ → List ((List Bool × List Bool) × List Bool)} - {elem : γ → (List Bool × List Bool) × List Bool} - (hlist : ComputableTidilyInPolyTime list encIn - (encList (encPair (encPair encBits encBits) encBits))) - (helem : ComputableTidilyInPolyTime elem encIn - (encPair (encPair encBits encBits) encBits)) : - ComputableTidilyInPolyTime (fun a => (list a).contains (elem a)) encIn encBool := by - have heq : (fun a => (list a).contains (elem a)) = - (fun a => (list a).any (fun x => elem a == x)) := by - funext a - rw [Bool.eq_iff_iff, List.contains_iff_mem, List.any_eq_true] - simp only [beq_iff_eq] - exact ⟨fun h => ⟨elem a, h, rfl⟩, fun ⟨_, h, heq⟩ => heq ▸ h⟩ - rw [heq] - exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist - (ComputableTidilyInPolyTime.beq (encB := encPair (encPair encBits encBits) encBits) - (helem.comp (ComputableTidilyInPolyTime.fst _ _)) - (ComputableTidilyInPolyTime.snd _ _)) - /-- Deciding `List.Nodup` on a framed list of bit strings is computable tidily in polynomial time. -/ -@[fun_prop] -theorem computableTidilyInPolyTime_decide_nodup {γ : Type} {encIn : γ ↪ List Bool} +@[local fun_prop] +private theorem computableTidilyInPolyTime_decide_nodup {γ : Type} {encIn : γ ↪ List Bool} {list : γ → List (List Bool)} (hlist : ComputableTidilyInPolyTime list encIn (encList encBits)) : ComputableTidilyInPolyTime (fun a => decide (list a).Nodup) encIn encBool := by @@ -1748,7 +1709,7 @@ theorem computableTidilyInPolyTime_decide_nodup {γ : Type} {encIn : γ ↪ List /-- The unframed prefix and remaining suffix of any bit list satisfy `2 * (unframe v).length + (dropFrame v).length ≤ v.length`. -/ -theorem length_unframe_add_dropFrame_le : +private theorem length_unframe_add_dropFrame_le : ∀ v : List Bool, 2 * (unframe v).length + (dropFrame v).length ≤ v.length | [] | [true] => by simp [unframe, dropFrame] | false :: v => by simp [unframe, dropFrame] @@ -2194,68 +2155,6 @@ theorem eval_sufCmaGame_eq_freshPair_of_unique_tag (M : NonceMACScheme) · simp [Bool.eq_false_iff.mpr hnonce] · simp [Bool.eq_false_iff.mpr hmsg] -/-- For any `NonceMACScheme` whose valid `(nonce, tag)` pairs on `M.msgLen n`-bit messages under -supported secret keys agree with every `(nonce', tag')` produced on that message, `sufCmaGame` and -`eufCmaGame` have the exact same output distribution. -/ -theorem eval_sufCmaGame_eq_eufCmaGame_of_unique_tag (M : NonceMACScheme) - (huniq : ∀ n sk, sk ∈ (ProbComp.eval (M.keyGen n)).support → - ∀ msg, msg.length = M.msgLen n → - ∀ nonce, nonce.length = M.nonceLen n → ∀ nonce' tag tag', - M.verify sk msg nonce tag = true → - tag' ∈ (ProbComp.eval (M.sign sk msg nonce')).support → - nonce' = nonce ∧ tag' = tag) - (adversary : NonceMACForger) (n : ℕ) : - ProbComp.eval (M.sufCmaGame adversary n) = - ProbComp.eval (M.eufCmaGame adversary n) := by - simp only [sufCmaGame, eufCmaGame, ProbComp.eval_bind, ProbComp.eval_pure] - refine PMF.bind_congr_on_support _ _ _ fun sk hsk => ?_ - refine PMF.bind_congr_on_support _ _ _ fun ⟨⟨⟨msg, nonce⟩, tag⟩, queriedTriples⟩ hout => ?_ - have hinv := M.mem_support_signingPairOracle sk (adversary n []) - ((msg, nonce), tag) queriedTriples hout - congr 1 - by_cases hmsg : (msg.length == M.msgLen n) = true - · by_cases hnonce : (nonce.length == M.nonceLen n) = true - · by_cases hver : M.verify sk msg nonce tag = true - · have hmsgLen : msg.length = M.msgLen n := beq_iff_eq.mp hmsg - have hnonceLen : nonce.length = M.nonceLen n := beq_iff_eq.mp hnonce - have hmem_iff : ((msg, nonce), tag) ∈ queriedTriples ↔ - msg ∈ queriedTriples.map (fun e => e.1.1) := by - rw [List.mem_map] - refine ⟨fun h => ⟨((msg, nonce), tag), h, rfl⟩, ?_⟩ - rintro ⟨⟨⟨qmsg, qnonce⟩, qtag⟩, hmemTriple, hmsg_eq⟩ - dsimp only at hmsg_eq - subst qmsg - have hqtag := hinv ((msg, qnonce), qtag) hmemTriple - obtain ⟨rfl, rfl⟩ := huniq n sk hsk msg hmsgLen nonce hnonceLen qnonce tag qtag hver hqtag - exact hmemTriple - simp only [hmsg, hnonce, hver, Bool.true_and, Bool.and_true, List.contains_eq_mem, - decide_eq_decide.mpr hmem_iff] - · simp [Bool.eq_false_iff.mpr hver] - · simp [Bool.eq_false_iff.mpr hnonce] - · simp [Bool.eq_false_iff.mpr hmsg] - -/-- Under the unique-`(nonce, tag)` hypothesis of `eval_sufCmaGame_eq_eufCmaGame_of_unique_tag`, -strong unforgeability (`SUFCMA`) is equivalent to fresh-message unforgeability (`EUFCMA`). -/ -theorem sufCma_iff_eufCma_of_unique_tag (M : NonceMACScheme) - (huniq : ∀ n sk, sk ∈ (ProbComp.eval (M.keyGen n)).support → - ∀ msg, msg.length = M.msgLen n → - ∀ nonce, nonce.length = M.nonceLen n → ∀ nonce' tag tag', - M.verify sk msg nonce tag = true → - tag' ∈ (ProbComp.eval (M.sign sk msg nonce')).support → - nonce' = nonce ∧ tag' = tag) : - M.SUFCMA ↔ M.EUFCMA := by - refine ⟨SUFCMA.eufCma, fun h => ?_⟩ - apply SUFCMA.of_negligible - intro adversary hadversary - refine (h.negligible adversary hadversary).congr fun n => ?_ - rw [M.eval_sufCmaGame_eq_eufCmaGame_of_unique_tag huniq adversary n] - end NonceMACScheme -/-- Alias for `NonceMACScheme.SUFCMA`. -/ -abbrev NonceSUFCMA := NonceMACScheme.SUFCMA - -/-- Alias for `NonceMACScheme.EUFCMA`. -/ -abbrev NonceEUFCMA := NonceMACScheme.EUFCMA - end Cslib.Crypto diff --git a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean index 686ff625dd..fd67d6cb2d 100644 --- a/Complexity/Crypto/Protocols/MAC/CarterWegman.lean +++ b/Complexity/Crypto/Protocols/MAC/CarterWegman.lean @@ -300,7 +300,8 @@ This module formalizes: `Cslib.Crypto.PseudorandomFunction.eufCma_carterWegmanNonceMAC`: full nonce-based Carter–Wegman security (Boneh–Shoup Attack Game 7.4 and Theorem 7.10). * `Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_randomNonceFnHandler`, - `probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler`, +`Cslib.Crypto.Protocols.CarterWegman.probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler` + (`ProbOracleComp` lift), `Cslib.Crypto.Protocols.CarterWegman.randomNonceSimHandler_not_nodup_le`, `Cslib.Crypto.Protocols.CarterWegman.probOracleComp_randomNonceSimHandler_not_nodup_le`, `Cslib.Crypto.Protocols.CarterWegman.seed_uniform_probOracleComp_checkRandomNonceSUF_le`, @@ -2766,8 +2767,57 @@ private theorem interpret_unifFin {α : Type} (p : ProbComp α) : OracleComp.interpret ProbComp.unifFin p = p := OracleComp.interpret_query_eq_self p +@[local fun_prop] +private theorem computableTidilyInPolyTime_contains {γ α : Type} [BEq α] [LawfulBEq α] + {encIn : γ ↪ List Bool} {encElem : α ↪ List Bool} + {list : γ → List α} {elem : γ → α} + (hlist : ComputableTidilyInPolyTime list encIn (encList encElem)) + (helem : ComputableTidilyInPolyTime elem encIn encElem) : + ComputableTidilyInPolyTime (fun a => (list a).contains (elem a)) encIn encBool := by + have heq : (fun a => (list a).contains (elem a)) = + (fun a => (list a).any (fun x => elem a == x)) := by + funext a + rw [Bool.eq_iff_iff, List.contains_iff_mem, List.any_eq_true] + simp only [beq_iff_eq] + exact ⟨fun h => ⟨elem a, h, rfl⟩, fun ⟨_, h, heq⟩ => heq ▸ h⟩ + rw [heq] + exact ComputableTidilyInPolyTime.anyWithInput (test := fun a x => elem a == x) hlist + (ComputableTidilyInPolyTime.beq (encB := encElem) + (helem.comp (ComputableTidilyInPolyTime.fst _ _)) + (ComputableTidilyInPolyTime.snd _ _)) + +@[local fun_prop] +private theorem computableTidilyInPolyTime_decide_nodup {γ : Type} {encIn : γ ↪ List Bool} + {list : γ → List (List Bool)} + (hlist : ComputableTidilyInPolyTime list encIn (encList encBits)) : + ComputableTidilyInPolyTime (fun a => decide (list a).Nodup) encIn encBool := by + have heq : (fun a => decide (list a).Nodup) = + (fun a => (list a).all (fun x => (list a).count x == 1)) := by + funext a + rw [Bool.eq_iff_iff, decide_eq_true_eq, List.all_eq_true, List.nodup_iff_count_le_one] + simp only [beq_iff_eq] + refine ⟨fun h x hx => ?_, fun h x => ?_⟩ + · have hle := h x + have hpos := List.count_pos_iff.mpr hx + omega + · by_cases hx : x ∈ list a + · exact (h x hx).le + · simp [List.count_eq_zero.mpr hx] + rw [heq] + exact ComputableTidilyInPolyTime.allWithInput (test := fun a x => (list a).count x == 1) + hlist (by polytime) + +private theorem length_unframe_add_dropFrame_le : + ∀ v : List Bool, 2 * (unframe v).length + (dropFrame v).length ≤ v.length + | [] | [true] => by simp [unframe, dropFrame] + | false :: v => by simp [unframe, dropFrame] + | true :: b :: v => by + have ih := length_unframe_add_dropFrame_le v + simp only [unframe, dropFrame, List.length_cons] + omega + /-- **Computational nonce-based Carter–Wegman MAC (`NonceMACScheme`)** -([BonehShoup2023], Section 7.5, Figure 7.3 and Theorem 7.10, p. 274): +([BonehShoup2023], Section 7.5.1, Attack Game 7.4 and Theorem 7.10, p. 274): given a polynomial-time message-length schedule `msgLen : ℕ → ℕ`, a strict-PPT hash-key sampler `seed : ℕ → ProbComp (List Bool)`, a polynomial-time hash evaluator `hash : ℕ → List Bool → List Bool → List Bool`, and a polynomial-time PRF family