Documentation

Complexity.Crypto.Protocols.MAC.CarterWegman

Carter–Wegman message authentication codes from Δ-universal hashing #

Wegman and Carter [WC81] observed that an ε-almost-Δ-universal (ε-DUF / ε-AXU) hash family hash : K → M → Y into a finite additive group Y (Cslib.Probability.IsDeltaUniversalHash) yields an unconditional message authentication code when each hash digest hash k m is masked by a uniform one-time pad r ∈ Y:

For every fixed hash key k and message m, left addition by hash k m is a bijection on Y, so a uniform pad r ← PMF.uniformOfFintype Y makes the tag t = hash k m + r uniformly distributed on Y and independent of k, with r = -hash k m + t (map_sign_eq_uniform, bind_uniform_sign). After seeing (m, t), any forgery attempt (m', t') with m' ≠ m verifies under r = -hash k m + t if and only if

hash k m' - hash k m = t' - t (verify_neg_add_eq_true_iff).

Since the adversary's view (m, t) is independent of k, IsDeltaUniversalHash seed hash ε bounds the probability of this difference equation over k ← seed by at most ε ([BS23], Section 7.6, Lemma 7.11 and Theorem 7.12).

This module formalizes:

  1. Algebraic and resampling properties (sign, verify, map_sign_eq_uniform, bind_uniform_sign) over any finite additive group Y.
  2. Zero-query forgery (zeroQueryGame, zeroQueryGame_apply_true): without a signing query, any forgery attempt succeeds with probability at most (and in fact equal to) 1 / |Y|.
  3. Adaptive one-time EUF-CMA and SUF-CMA security (OneTimeForger, oneTimeGame, oneTimeStrongGame, oneTimeStrongGame_eq_oneTimeGame, oneTimeGame_le, oneTimeStrongGame_le): because each (k, r, m) admits a unique valid tag, strong unforgeability ((m', t') ≠ (m, t)) and ordinary unforgeability (m' ≠ m) coincide and are bounded by ε ([BS23], Section 7.6, Lemma 7.11 and Theorem 7.12).
  4. Adaptive multi-query issued-counter / issued-slot Carter–Wegman MAC (CounterForger, counterSlotGame, counterGame, counterStrongGame, counterStrongGame_eq_counterSlotGame, counterSlotGame_le, counterGame_le, counterStrongGame_le): when each signing query draws an independent uniform pad r_i ← PMF.uniformOfFintype Y (recorded at counter index i), the entire adaptive query transcript is independent of the hash key k, so any adaptive OracleComp forger (making any number of queries) targeting an issued counter index idx < pads.length has forgery probability at most ε under issued-slot message freshness (counterSlotGame), issued-counter global message freshness (counterGame), and issued-slot strong pair freshness (counterStrongGame), with zero degradation in the number of queries [WC81]. Unissued counter indices (pads[idx]? = none) are rejected (false), so zero-query success in the issued-counter games is 0 (whereas the standalone zeroQueryGame has success 1 / |Y|); a fresh-counter experiment that accepts unissued nonces against fresh pads is separate scope.
  5. Arbitrary-pad hybrid decomposition and the one-query, fixed-nonce PRF-pad reduction (maskedOneTimeGame, padDistinguisher, maskedOneTimeGame_toReal_le, maskedOneTimeGame_toReal_le_add_advantage, prfPadDist, prfOneTimeGame, prfOneTimeStrongGame, prfPadDistinguisher, prfOneTimeGame_le, prfOneTimeStrongGame_le, prfOneTimeGame_ofProbComp_le, isOraclePPT_prfPadDistinguisher, wordProbPadTest, isPPTOn_wordProbPadTest, isOraclePPT_prfPadDistinguisher_wordProbPadTest, PseudorandomFunction.negligible_prfOneTimeGame, PseudorandomFunction.negligible_prfOneTimeStrongGame, PseudorandomFunction.negligible_prfOneTimeGame_wordProbPadTest, PseudorandomFunction.negligible_prfOneTimeStrongGame_wordProbPadTest): replacing the uniform pad r ← PMF.uniformOfFintype Y with any pad distribution padDist : PMF Y bounds the real forgery probability by ε.toReal plus the distinguishing advantage of padDistinguisher between padDist and PMF.uniformOfFintype Y (after [BS23], Section 7.4). In the one-query, fixed-nonce case where Y = BitString n and the pad is generated by evaluating family at the fixed nonce List.replicate n false under a uniform n-bit key (prfPadDist family n), the single-query OracleDistinguisher adapter prfPadDistinguisher realizes the real and ideal pad experiments inside prfRealGame and prfIdealGame at each parameter n, is uniformly strict oracle-PPT (IsOraclePPT encBool) whenever the pad test is uniformly strict PPT, and yields negligible forgery probability under PseudorandomFunction family and Negligible ε.
  6. Multi-query fresh-nonce PRF-masked Carter–Wegman MAC (counterSeqHandler, maskedCounterSlotGame, maskedCounterGame, maskedCounterStrongGame, counterPadSeqDistinguisher, prfPadSeqDist, prfCounterSlotGame, prfCounterGame, prfCounterStrongGame, prfMultiPadDistinguisher, prfCounterSlotGame_le, prfCounterGame_le, prfCounterStrongGame_le, isOraclePPT_prfMultiPadDistinguisher, PseudorandomFunction.negligible_prfCounterSlotGame, PseudorandomFunction.negligible_prfCounterGame, PseudorandomFunction.negligible_prfCounterStrongGame): when the i-th signing query uses a PRF pad BitString.ofList n (prfOracle family n key (nonce n i)) at pairwise distinct n-bit nonces nonce n 0, ..., nonce n (Q n - 1), any Q n-query-bounded adaptive CounterForger has forgery probability at most ε.toReal plus the concrete Q n-query PRF distinguishing advantage of prfMultiPadDistinguisher Q nonce test, and negligible forgery probability when family is a PseudorandomFunction and ε is Negligible (after [BS23], Section 7.5, Theorem 7.10). This models the nonce-based Carter–Wegman construction under two restrictions compared to Boneh–Shoup Attack Game 7.4: (a) the signer's counter schedule nonce n i fixes the nonces rather than letting the adversary choose distinct nonces, and (b) checkCounterSlot / checkCounterEUF / checkCounterSUF accept forgeries only at issued counter slots (pads[idx]? = some r) and reject unissued idx, which removes the 1 / |T| unissued-nonce guessing term.
  7. Full nonce-based Carter–Wegman MAC (NonceForger, nonceFnHandler, nonceSimHandler, reconstructPadFn, checkNonceSUF, checkNonceEUF, nonceStrongGame, nonceGame, nonceStrongGame_le_max, nonceStrongGame_le, nonceGame_le_max, nonceGame_le, maskedNonceStrongGame, maskedNonceGame, nonceFnDistinguisher, prfFnDist, prfNonceStrongGame, prfNonceGame, prfNonceStrongGame_le_of_distinguisher, prfNonceGame_le_of_distinguisher, PseudorandomFunction.negligible_prfNonceStrongGame, 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 ([BS23], 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, maskedRandomNonceStrongGame, maskedRandomNonceGame, randomNonceFnDistinguisher, prfRandomNonceStrongGame, prfRandomNonceGame, prfRandomNonceStrongGame_le_of_distinguisher, prfRandomNonceGame_le_of_distinguisher, PseudorandomFunction.negligible_prfRandomNonceStrongGame, 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 ([BS23], 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, 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 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|).

Main definitions #

Main results #

References #

Core Carter–Wegman signing, verification, and pad resampling #

source
def Cslib.Crypto.Protocols.CarterWegman.sign {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] (hash : K → M → Y) (k : K) (r : Y) (m : M) :
Y

Carter–Wegman tag generation ([WC81]; [BS23], Section 7.4): mask the hash digest hash k m by adding the pad r.

Instances For
    source
    def Cslib.Crypto.Protocols.CarterWegman.verify {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq Y] (hash : K → M → Y) (k : K) (r : Y) (m : M) (t : Y) :
    Bool

    Carter–Wegman tag verification: check whether hash k m + r = t.

    Instances For
      source
      @[simp]
      theorem Cslib.Crypto.Protocols.CarterWegman.verify_eq_true_iff {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq Y] (hash : K → M → Y) (k : K) (r : Y) (m : M) (t : Y) :
      verify hash k r m t = true ↔ hash k m + r = t
      source
      @[simp]
      theorem Cslib.Crypto.Protocols.CarterWegman.verify_sign {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq Y] (hash : K → M → Y) (k : K) (r : Y) (m : M) :
      verify hash k r m (sign hash k r m) = true
      source
      theorem Cslib.Crypto.Protocols.CarterWegman.eq_sign_of_verify_eq_true {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq Y] {hash : K → M → Y} {k : K} {r : Y} {m : M} {t : Y} (h : verify hash k r m t = true) :
      t = sign hash k r m

      Every valid tag for (k, r, m) equals sign hash k r m.

      source
      theorem Cslib.Crypto.Protocols.CarterWegman.sign_eq_iff_eq_neg_add {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] (hash : K → M → Y) (k : K) (r : Y) (m : M) (t : Y) :
      sign hash k r m = t ↔ r = -hash k m + t

      Solving for the pad r from a message–tag pair (m, t): sign hash k r m = t ↔ r = -hash k m + t.

      source
      theorem Cslib.Crypto.Protocols.CarterWegman.verify_neg_add_eq_true_iff {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq Y] (hash : K → M → Y) (k : K) (m m' : M) (t t' : Y) :
      verify hash k (-hash k m + t) m' t' = true ↔ hash k m' - hash k m = t' - t

      After observing tag t = hash k m + r (so r = -hash k m + t), a candidate pair (m', t') verifies if and only if hash k m' - hash k m = t' - t.

      source
      theorem Cslib.Crypto.Protocols.CarterWegman.verify_neg_add_decide {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq Y] (hash : K → M → Y) (k : K) (m m' : M) (t t' : Y) :
      verify hash k (-hash k m + t) m' t' = decide (hash k m' - hash k m = t' - t)

      Boolean form of verify_neg_add_eq_true_iff.

      source
      theorem Cslib.Crypto.Protocols.CarterWegman.decide_ne_pair_and_verify_eq {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (r : Y) (m : M) (p : M × Y) :
      (decide (p ≠ (m, sign hash k r m)) && verify hash k r p.1 p.2) = (decide (p.1 ≠ m) && verify hash k r p.1 p.2)

      Because (k, r, m) determines a unique valid tag sign hash k r m, pair freshness (m', t') ≠ (m, sign hash k r m) and message freshness m' ≠ m agree on all verifying pairs.

      source
      theorem Cslib.Crypto.Protocols.CarterWegman.map_sign_eq_uniform {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (m : M) :
      PMF.map (fun (x : Y) => sign hash k x m) (Probability.PMF.uniformOfFintype Y) = Probability.PMF.uniformOfFintype Y

      For a uniform pad r ← PMF.uniformOfFintype Y, the tag sign hash k r m is uniformly distributed on Y for every k and m.

      source
      theorem Cslib.Crypto.Protocols.CarterWegman.bind_uniform_sign {K : Type u_1} {M : Type u_2} {Y : Type u_3} [AddGroup Y] {α : Type u_4} [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (m : M) (f : Y → Y → PMF α) :
      ((Probability.PMF.uniformOfFintype Y).bind fun (r : Y) => f (sign hash k r m) r) = (Probability.PMF.uniformOfFintype Y).bind fun (t : Y) => f t (-hash k m + t)

      Pad-to-tag change of variables: sampling a uniform pad r ← PMF.uniformOfFintype Y and passing (sign hash k r m, r) to a continuation f is identical to sampling a uniform tag t ← PMF.uniformOfFintype Y and reconstructing r = -hash k m + t.

      Zero-query forgery experiment #

      source
      noncomputable def Cslib.Crypto.Protocols.CarterWegman.zeroQueryGame {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : PMF (M × Y)) :
      PMF Bool

      The zero-query forgery experiment: sample k ← seed, r ← PMF.uniformOfFintype Y, and (m', t') ← forger, and check whether verify hash k r m' t' = true.

      Instances For
        source
        theorem Cslib.Crypto.Protocols.CarterWegman.zeroQueryGame_apply_true {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : PMF (M × Y)) :
        (zeroQueryGame seed hash forger) true = (↑(Fintype.card Y))⁻¹

        Without any signing query, every forgery distribution forger : PMF (M × Y) succeeds with probability exactly 1 / |Y|, regardless of the hash family hash or key distribution seed.

        Adaptive one-time Carter–Wegman EUF-CMA and SUF-CMA (Boneh–Shoup Section 7.6) #

        source
        structure Cslib.Crypto.Protocols.CarterWegman.OneTimeForger (M Y : Type) :
        Type

        An adaptive one-time forger against a Carter–Wegman MAC: it chooses a signing query m ← query, receives its tag t = sign hash k r m, and outputs a candidate forgery (m', t') ← forge m t.

        • query : PMF M

          Distribution of the single signing query m.

        • forge : M → Y → PMF (M × Y)

          Forgery distribution given the queried message m and its tag t.

        Instances For
          source
          noncomputable def Cslib.Crypto.Protocols.CarterWegman.oneTimeGame {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) :
          PMF Bool

          The adaptive one-time EUF-CMA experiment ([BS23], Section 7.6, Lemma 7.11 and Theorem 7.12): the forger wins if m' ≠ m and verify hash k r m' t' = true.

          Instances For
            source
            noncomputable def Cslib.Crypto.Protocols.CarterWegman.oneTimeStrongGame {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) :
            PMF Bool

            The adaptive one-time SUF-CMA (strong unforgeability) experiment: the forger wins if (m', t') ≠ (m, sign hash k r m) and verify hash k r m' t' = true.

            Instances For
              source
              theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeStrongGame_eq_oneTimeGame {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) :
              oneTimeStrongGame seed hash forger = oneTimeGame seed hash forger

              Strong unforgeability and ordinary unforgeability coincide for the one-time Carter–Wegman MAC, because each (k, r, m) admits a unique valid tag.

              source
              theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_eq_bind_uniform {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) :
              oneTimeGame seed hash forger = forger.query.bind fun (m : M) => (Probability.PMF.uniformOfFintype Y).bind fun (t : Y) => (forger.forge m t).bind fun (p : M × Y) => seed.bind fun (k : K) => PMF.pure (decide (p.1 ≠ m) && verify hash k (-hash k m + t) p.1 p.2)

              Reformulation of oneTimeGame via bind_uniform_sign: the queried message m, uniform tag t, and candidate forgery p = (m', t') are sampled independently of the hash key k, which is drawn last to test verify hash k (-hash k m + t) m' t'.

              source
              theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_le {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : OneTimeForger M Y) :
              (oneTimeGame seed hash forger) true ≤ ε

              One-time Carter–Wegman EUF-CMA security ([BS23], Section 7.6, Lemma 7.11 and Theorem 7.12; [WC81]): if hash is ε-almost-Δ-universal under seed (IsDeltaUniversalHash seed hash ε), then every adaptive one-time forger succeeds with probability at most ε.

              source
              theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeStrongGame_le {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : OneTimeForger M Y) :
              (oneTimeStrongGame seed hash forger) true ≤ ε

              One-time Carter–Wegman SUF-CMA security: under IsDeltaUniversalHash seed hash ε, every adaptive one-time forger has strong-forgery probability at most ε.

              Adaptive multi-query issued-counter Carter–Wegman MAC #

              source
              structure Cslib.Crypto.Protocols.CarterWegman.CounterForger (M Y : Type) :
              Type 1

              An adaptive multi-query forger against an issued-counter Carter–Wegman MAC: it draws private coins s ← coins, makes any number of adaptive signing queries m : M via OracleComp (fun _ : M => Y) (receiving t_i = sign hash k r_i m_i under a fresh pad r_i for the i-th query), and outputs a target issued counter index idx : ℕ, message m' : M, and tag t' : Y.

              • Coins : Type

                Type of the forger's private coins.

              • coins : PMF self.Coins

                Distribution of the forger's private coins.

              • forge : self.Coins → OracleComp (fun (x : M) => Y) (ℕ × M × Y)

                Adaptive oracle program outputting (idx, m', t').

              Instances For
                source
                noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterRealHandler {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (m : M) :
                StateT (List (M × Y)) PMF Y

                Real counter Carter–Wegman signing handler: on query m, sample a fresh pad r ← PMF.uniformOfFintype Y, append (m, r) to the pad log, and return sign hash k r m.

                Instances For
                  source
                  noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterSimHandler {M Y : Type} [Fintype Y] [Nonempty Y] (m : M) :
                  StateT (List (M × Y)) PMF Y

                  Simulated key-independent tag handler: on query m, sample a fresh uniform tag t ← PMF.uniformOfFintype Y, append (m, t) to the message–tag transcript, and return t.

                  Instances For
                    source
                    def Cslib.Crypto.Protocols.CarterWegman.transcriptToPads {K M Y : Type} [AddGroup Y] (hash : K → M → Y) (k : K) (tr : List (M × Y)) :
                    List (M × Y)

                    Reconstruct the pad log [(m_i, -hash k m_i + t_i)] from a message–tag transcript [(m_i, t_i)].

                    Instances For
                      source
                      theorem Cslib.Crypto.Protocols.CarterWegman.run_interpret_counterRealHandler {K M Y : Type} [AddGroup Y] {α : Type} [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (prog : OracleComp (fun (x : M) => Y) α) (tr : List (M × Y)) :
                      (OracleComp.interpret (counterRealHandler hash k) prog).run (transcriptToPads hash k tr) = PMF.map (fun (x : α × List (M × Y)) => (x.1, transcriptToPads hash k x.2)) ((OracleComp.interpret counterSimHandler prog).run tr)

                      Running any adaptive OracleComp program against counterRealHandler hash k from transcriptToPads hash k tr has the exact distribution of running it against the key-independent counterSimHandler from tr and applying transcriptToPads hash k to the final transcript.

                      source
                      def Cslib.Crypto.Protocols.CarterWegman.checkCounterSlot {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (pads : List (M × Y)) (out : ℕ × M × Y) :
                      Bool

                      Issued-slot message-freshness verification predicate on a pad log pads: the target counter idx was issued (pads[idx]? = some (m_idx, r_idx), returning false on unissued indices), m' ≠ m_idx, and verify hash k r_idx m' t' = true.

                      Instances For
                        source
                        def Cslib.Crypto.Protocols.CarterWegman.checkCounterEUF {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (pads : List (M × Y)) (out : ℕ × M × Y) :
                        Bool

                        Issued-counter global-message-freshness EUF-CMA verification predicate on a pad log pads: the target counter idx was issued (pads[idx]? = some (_, r_idx), returning false on unissued indices), m' was never queried in any issued slot (!(pads.map Prod.fst).contains m'), and verify hash k r_idx m' t' = true.

                        Instances For
                          source
                          def Cslib.Crypto.Protocols.CarterWegman.checkCounterSUF {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (pads : List (M × Y)) (out : ℕ × M × Y) :
                          Bool

                          Issued-slot strong SUF-CMA verification predicate on a pad log pads: the target counter idx was issued (pads[idx]? = some (m_idx, r_idx), returning false on unissued indices), the pair (m', t') differs from the pair (m_idx, sign hash k r_idx m_idx) issued at counter idx, and verify hash k r_idx m' t' = true.

                          Instances For
                            source
                            theorem Cslib.Crypto.Protocols.CarterWegman.checkCounterSUF_eq_checkCounterSlot {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (pads : List (M × Y)) (out : ℕ × M × Y) :
                            checkCounterSUF hash k pads out = checkCounterSlot hash k pads out

                            Issued-slot SUF-CMA and issued-slot EUF-CMA checks are identical on every pad log and output.

                            source
                            theorem Cslib.Crypto.Protocols.CarterWegman.checkCounterEUF_imp_checkCounterSlot {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (pads : List (M × Y)) (out : ℕ × M × Y) :
                            checkCounterEUF hash k pads out = true → checkCounterSlot hash k pads out = true

                            Issued-counter global message freshness implies issued-slot message freshness at the target counter idx.

                            source
                            noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterSlotGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : CounterForger M Y) :
                            PMF Bool

                            The issued-slot EUF-CMA experiment for the counter Carter–Wegman MAC (unissued indices idx are rejected).

                            Instances For
                              source
                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : CounterForger M Y) :
                              PMF Bool

                              The issued-counter global-message-freshness EUF-CMA experiment for the counter Carter–Wegman MAC (unissued indices idx are rejected).

                              Instances For
                                source
                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterStrongGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : CounterForger M Y) :
                                PMF Bool

                                The issued-slot strong SUF-CMA experiment for the counter Carter–Wegman MAC (unissued indices idx are rejected).

                                Instances For
                                  source
                                  theorem Cslib.Crypto.Protocols.CarterWegman.counterStrongGame_eq_counterSlotGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : CounterForger M Y) :
                                  counterStrongGame seed hash forger = counterSlotGame seed hash forger

                                  Issued-slot strong unforgeability (counterStrongGame) and issued-slot EUF-CMA (counterSlotGame) have identical outcome distributions.

                                  source
                                  theorem Cslib.Crypto.Protocols.CarterWegman.counterGame_le_counterSlotGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : CounterForger M Y) :
                                  (counterGame seed hash forger) true ≤ (counterSlotGame seed hash forger) true

                                  Issued-counter global-message-freshness EUF-CMA success probability is at most issued-slot EUF-CMA success probability.

                                  source
                                  theorem Cslib.Crypto.Protocols.CarterWegman.counterSlotGame_le {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : CounterForger M Y) :
                                  (counterSlotGame seed hash forger) true ≤ ε

                                  Multi-query issued-slot Carter–Wegman security ([WC81]; [BS23], Section 7.4): under IsDeltaUniversalHash seed hash ε, every adaptive multi-query forger succeeds in counterSlotGame with probability at most ε, with zero degradation in the number of signing queries.

                                  source
                                  theorem Cslib.Crypto.Protocols.CarterWegman.counterGame_le {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : CounterForger M Y) :
                                  (counterGame seed hash forger) true ≤ ε

                                  Multi-query issued-counter Carter–Wegman EUF-CMA security: under IsDeltaUniversalHash seed hash ε, every adaptive multi-query forger has issued-counter EUF-CMA forgery probability at most ε.

                                  source
                                  theorem Cslib.Crypto.Protocols.CarterWegman.counterStrongGame_le {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : CounterForger M Y) :
                                  (counterStrongGame seed hash forger) true ≤ ε

                                  Multi-query issued-slot Carter–Wegman SUF-CMA security: under IsDeltaUniversalHash seed hash ε, every adaptive multi-query forger has issued-slot SUF-CMA forgery probability at most ε.

                                  Pseudorandom-pad hybrid decomposition (after Boneh–Shoup Section 7.4) #

                                  source
                                  noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padDist : PMF Y) (hash : K → M → Y) (forger : OneTimeForger M Y) :
                                  PMF Bool

                                  The one-time Carter–Wegman experiment with an arbitrary pad distribution padDist : PMF Y (such as a pseudorandom function output F(k₂, nonce)).

                                  Instances For
                                    source
                                    noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeStrongGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padDist : PMF Y) (hash : K → M → Y) (forger : OneTimeForger M Y) :
                                    PMF Bool

                                    The strong one-time Carter–Wegman experiment with an arbitrary pad distribution padDist : PMF Y.

                                    Instances For
                                      source
                                      @[simp]
                                      theorem Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_uniform {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) :
                                      maskedOneTimeGame seed (Probability.PMF.uniformOfFintype Y) hash forger = oneTimeGame seed hash forger
                                      source
                                      theorem Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeStrongGame_eq_maskedOneTimeGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padDist : PMF Y) (hash : K → M → Y) (forger : OneTimeForger M Y) :
                                      maskedOneTimeStrongGame seed padDist hash forger = maskedOneTimeGame seed padDist hash forger
                                      source
                                      noncomputable def Cslib.Crypto.Protocols.CarterWegman.padDistinguisher {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : OneTimeForger M Y) (r : Y) :
                                      PMF Bool

                                      The induced pad distinguisher Y → PMF Bool that samples k ← seed, simulates the one-time Carter–Wegman experiment using the supplied pad r : Y, and outputs true iff the forger produces a valid forgery.

                                      Instances For
                                        source
                                        theorem Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_eq_bind_padDistinguisher {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padDist : PMF Y) (hash : K → M → Y) (forger : OneTimeForger M Y) :
                                        maskedOneTimeGame seed padDist hash forger = padDist.bind (padDistinguisher seed hash forger)

                                        maskedOneTimeGame is equivalent to sampling r ← padDist and running padDistinguisher seed hash forger r.

                                        source
                                        theorem Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (padDist : PMF Y) (forger : OneTimeForger M Y) :
                                        ((maskedOneTimeGame seed padDist hash forger) true).toReal ≤ ε.toReal + |((padDist.bind (padDistinguisher seed hash forger)) true).toReal - (((Probability.PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)) true).toReal|

                                        Pseudorandom-pad Carter–Wegman bound (after [BS23], Section 7.4): if hash is ε-almost-Δ-universal (ε ≠ ⊤), then the real-valued forgery probability under any pad distribution padDist : PMF Y is bounded by ε.toReal plus the distinguishing gap of padDistinguisher between padDist and PMF.uniformOfFintype Y.

                                        source
                                        theorem Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeGame_toReal_le_add_advantage {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (padDist : PMF Y) (forger : OneTimeForger M Y) :
                                        ((maskedOneTimeGame seed padDist hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (padDist.bind (padDistinguisher seed hash forger)) ((Probability.PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)))

                                        Game.advantage form of maskedOneTimeGame_toReal_le (after [BS23], Section 7.4): the real-valued forgery probability under padDist is bounded by ε.toReal plus Game.advantage between padDist.bind (padDistinguisher seed hash forger) and (PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger).

                                        source
                                        theorem Cslib.Crypto.Protocols.CarterWegman.maskedOneTimeStrongGame_toReal_le_add_advantage {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (padDist : PMF Y) (forger : OneTimeForger M Y) :
                                        ((maskedOneTimeStrongGame seed padDist hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (padDist.bind (padDistinguisher seed hash forger)) ((Probability.PMF.uniformOfFintype Y).bind (padDistinguisher seed hash forger)))

                                        Strong-unforgeability version of maskedOneTimeGame_toReal_le_add_advantage.

                                        source
                                        noncomputable def Cslib.Crypto.Protocols.CarterWegman.OneTimeForger.ofProbComp {M Y : Type} (query : ProbComp M) (forge : M → Y → ProbComp (M × Y)) :
                                        OneTimeForger M Y

                                        Construct a OneTimeForger from ProbComp query and forgery programs.

                                        Instances For
                                          source
                                          def Cslib.Crypto.Protocols.CarterWegman.probPadTest {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : ProbComp K) (hash : K → M → Y) (query : ProbComp M) (forge : M → Y → ProbComp (M × Y)) (r : Y) :
                                          ProbComp Bool

                                          Executable ProbComp simulation of the one-time Carter–Wegman experiment with a supplied pad r : Y, given ProbComp samplers for the hash key seed, signing query query, and forgery attempt forge.

                                          Instances For
                                            source
                                            @[simp]
                                            theorem Cslib.Crypto.Protocols.CarterWegman.eval_probPadTest {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : ProbComp K) (hash : K → M → Y) (query : ProbComp M) (forge : M → Y → ProbComp (M × Y)) (r : Y) :
                                            (probPadTest seed hash query forge r).eval = padDistinguisher seed.eval hash (OneTimeForger.ofProbComp query forge) r

                                            One-query, fixed-nonce PRF-pad reduction (after Boneh–Shoup Section 7.4) #

                                            source
                                            noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfPadDist (family : List Bool → List Bool → List Bool) (n : ℕ) :
                                            PMF (BitString n)

                                            The one-time pad distribution on BitString n obtained by sampling a uniform n-bit PRF key key ← BitString.uniformList n and evaluating family key (List.replicate n false).

                                            Instances For
                                              source
                                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : OneTimeForger M (BitString n)) :
                                              PMF Bool

                                              The one-query, fixed-nonce PRF-masked Carter–Wegman EUF-CMA experiment (after [BS23], Section 7.4): the pad r : BitString n is generated by evaluating family on a uniform n-bit PRF key at the fixed nonce List.replicate n false.

                                              Instances For
                                                source
                                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : OneTimeForger M (BitString n)) :
                                                PMF Bool

                                                The one-query, fixed-nonce PRF-masked Carter–Wegman SUF-CMA experiment (after [BS23], Section 7.4).

                                                Instances For
                                                  source
                                                  theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_eq_prfOneTimeGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : OneTimeForger M (BitString n)) :
                                                  prfOneTimeStrongGame seed family n hash forger = prfOneTimeGame seed family n hash forger
                                                  source
                                                  def Cslib.Crypto.Protocols.CarterWegman.prfPadDistinguisher (test : (k : ℕ) → BitString k → ProbComp Bool) :
                                                  OracleDistinguisher

                                                  Single-query PRF OracleDistinguisher induced by a family of ProbComp pad tests test : (k : ℕ) → BitString k → ProbComp Bool: at security parameter n, query the oracle once at the fixed nonce List.replicate n false and run test n on the n-bit view of the reply.

                                                  Instances For
                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfPadDistinguisher (family : List Bool → List Bool → List Bool) (test : (k : ℕ) → BitString k → ProbComp Bool) (n : ℕ) :
                                                    (prfRealGame family (prfPadDistinguisher test) n).eval = (prfPadDist family n).bind fun (r : BitString n) => (test n r).eval

                                                    In prfRealGame, prfPadDistinguisher test evaluates test n on a pad drawn from prfPadDist family n.

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfPadDistinguisher (test : (k : ℕ) → BitString k → ProbComp Bool) (n : ℕ) :
                                                    (prfIdealGame (prfPadDistinguisher test) n).eval = (Probability.PMF.uniformOfFintype (BitString n)).bind fun (r : BitString n) => (test n r).eval

                                                    In prfIdealGame, prfPadDistinguisher test evaluates test n on a uniform pad r ← PMF.uniformOfFintype (BitString n).

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le_of_distinguisher {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) (D : OracleDistinguisher) (hreal : (prfRealGame family D n).eval = (prfPadDist family n).bind (padDistinguisher seed hash forger)) (hideal : (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n)).bind (padDistinguisher seed hash forger)) :
                                                    ((prfOneTimeGame seed family n hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family D n).eval (prfIdealGame D n).eval)

                                                    Exact single-query PRF-pad reduction for an explicit OracleDistinguisher in the one-query, fixed-nonce case (after [BS23], Section 7.4): if D simulates padDistinguisher seed hash forger in both prfRealGame and prfIdealGame at parameter n, then the real-valued one-time forgery probability is at most ε.toReal plus the concrete PRF distinguishing advantage of D at n.

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) (test : (k : ℕ) → BitString k → ProbComp Bool) (htest : ∀ (r : BitString n), padDistinguisher seed hash forger r = (test n r).eval) :
                                                    ((prfOneTimeGame seed family n hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfPadDistinguisher test) n).eval (prfIdealGame (prfPadDistinguisher test) n).eval)

                                                    Exact single-query PRF-pad reduction for prfOneTimeGame in the one-query, fixed-nonce case (after [BS23], Section 7.4): replacing the uniform pad r ← PMF.uniformOfFintype (BitString n) with the fixed-nonce PRF pad prfPadDist family n bounds the real-valued one-time forgery probability at parameter n by ε.toReal plus the concrete PRF distinguishing advantage of prfPadDistinguisher test between prfRealGame and prfIdealGame. Admissibility (IsOraclePPT encBool) and the asymptotic corollary from PseudorandomFunction family are not asserted here.

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger M (BitString n)) (test : (k : ℕ) → BitString k → ProbComp Bool) (htest : ∀ (r : BitString n), padDistinguisher seed hash forger r = (test n r).eval) :
                                                    ((prfOneTimeStrongGame seed family n hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfPadDistinguisher test) n).eval (prfIdealGame (prfPadDistinguisher test) n).eval)

                                                    Exact single-query PRF-pad reduction for prfOneTimeStrongGame in the one-query, fixed-nonce case (after [BS23], Section 7.4); admissibility (IsOraclePPT encBool) and the asymptotic PseudorandomFunction corollary are not asserted here.

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_ofProbComp_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : ProbComp K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed.eval hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (query : ProbComp M) (forge : M → BitString n → ProbComp (M × BitString n)) :
                                                    ((prfOneTimeGame seed.eval family n hash (OneTimeForger.ofProbComp query forge)) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfPadDistinguisher fun (x : ℕ) (r : BitString x) => probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n).eval (prfIdealGame (prfPadDistinguisher fun (x : ℕ) (r : BitString x) => probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n).eval)

                                                    Exact single-query PRF-pad reduction for ProbComp samplers and forgers in the one-query, fixed-nonce case (after [BS23], Section 7.4): at parameter n, any ProbComp hash-key sampler seed, query program query, and forgery program forge induce the single-query PRF distinguisher via probPadTest, without asserting IsOraclePPT encBool admissibility or an asymptotic PseudorandomFunction corollary.

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeStrongGame_ofProbComp_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : ProbComp K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed.eval hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (query : ProbComp M) (forge : M → BitString n → ProbComp (M × BitString n)) :
                                                    ((prfOneTimeStrongGame seed.eval family n hash (OneTimeForger.ofProbComp query forge)) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfPadDistinguisher fun (x : ℕ) (r : BitString x) => probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n).eval (prfIdealGame (prfPadDistinguisher fun (x : ℕ) (r : BitString x) => probPadTest seed hash query forge (BitString.ofList n (List.ofFn r))) n).eval)

                                                    Strong-unforgeability version of prfOneTimeGame_ofProbComp_le.

                                                    source
                                                    theorem Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfPadDistinguisher {test : (k : ℕ) → BitString k → ProbComp Bool} (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool) => test p.1 (BitString.ofList p.1 p.2)) :
                                                    Probability.IsOraclePPT Turing.MultiTapeTM.encBool (prfPadDistinguisher test)

                                                    prfPadDistinguisher test is uniformly strict oracle-PPT (IsOraclePPT encBool) whenever running test n on the n-bit view of a raw pad word is uniformly strict PPT in (n, word).

                                                    source
                                                    def Cslib.Crypto.Protocols.CarterWegman.wordProbPadTest (seed : ℕ → ProbComp (List Bool)) (hash : ℕ → List Bool → List Bool → List Bool) (query : ℕ → ProbComp (List Bool)) (forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)) (n : ℕ) (r : BitString n) :
                                                    ProbComp Bool

                                                    Executable ProbComp one-time pad test induced by a uniform word-level hash-key sampler seed, hash evaluator hash, signing query query, and forgery program forge: at security parameter n and pad r : BitString n, it runs probPadTest with digest BitString.ofList n (hash n k m) and candidate tag BitString.ofList n p.2.

                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem Cslib.Crypto.Protocols.CarterWegman.eval_wordProbPadTest (seed : ℕ → ProbComp (List Bool)) (hash : ℕ → List Bool → List Bool → List Bool) (query : ℕ → ProbComp (List Bool)) (forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)) (n : ℕ) (r : BitString n) :
                                                      (wordProbPadTest seed hash query forge n r).eval = padDistinguisher (seed n).eval (fun (k m : List Bool) => BitString.ofList n (hash n k m)) (OneTimeForger.ofProbComp (query n) fun (m : List Bool) (t : BitString n) => do let p ← forge n m (List.ofFn t) pure (p.1, BitString.ofList n p.2)) r
                                                      source
                                                      theorem Cslib.Crypto.Protocols.CarterWegman.isPPTOn_wordProbPadTest {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {query : ℕ → ProbComp (List Bool)} {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)} (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hquery : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits query) (hforge : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool × List Bool) => forge p.1 p.2.1 p.2.2) :
                                                      Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool) => wordProbPadTest seed hash query forge p.1 (BitString.ofList p.1 p.2)

                                                      If seed, hash, query, and forge are uniformly polynomial-time / strict PPT in their encoded inputs, then wordProbPadTest on the n-bit view of a raw pad word is uniformly strict PPT.

                                                      source
                                                      theorem Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfPadDistinguisher_wordProbPadTest {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {query : ℕ → ProbComp (List Bool)} {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)} (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hquery : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits query) (hforge : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool × List Bool) => forge p.1 p.2.1 p.2.2) :
                                                      Probability.IsOraclePPT Turing.MultiTapeTM.encBool (prfPadDistinguisher (wordProbPadTest seed hash query forge))

                                                      prfPadDistinguisher (wordProbPadTest seed hash query forge) is uniformly strict oracle-PPT (IsOraclePPT encBool) for any uniform polynomial-time / strict-PPT family (seed, hash, query, forge).

                                                      source
                                                      theorem Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) (forger : (n : ℕ) → Protocols.CarterWegman.OneTimeForger (M n) (BitString n)) (test : (k : ℕ) → BitString k → ProbComp Bool) (htest_eval : ∀ (n : ℕ) (r : BitString n), Protocols.CarterWegman.padDistinguisher (seed n) (hash n) (forger n) r = (test n r).eval) (htest_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool) => test p.1 (BitString.ofList p.1 p.2)) :
                                                      Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfOneTimeGame (seed n) family n (hash n) (forger n))

                                                      Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman EUF-CMA security (after [BS23], Section 7.4): if family is a PseudorandomFunction, each (seed n, hash n) is (ε n)-almost-Δ-universal with Negligible ε, and test is a uniformly strict-PPT pad test realizing padDistinguisher (seed n) (hash n) (forger n) at every n, then the one-time forgery probability Game.succProbability (prfOneTimeGame ...) is Negligible.

                                                      source
                                                      theorem Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) (forger : (n : ℕ) → Protocols.CarterWegman.OneTimeForger (M n) (BitString n)) (test : (k : ℕ) → BitString k → ProbComp Bool) (htest_eval : ∀ (n : ℕ) (r : BitString n), Protocols.CarterWegman.padDistinguisher (seed n) (hash n) (forger n) r = (test n r).eval) (htest_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (p : ℕ × List Bool) => test p.1 (BitString.ofList p.1 p.2)) :
                                                      Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfOneTimeStrongGame (seed n) family n (hash n) (forger n))

                                                      Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman SUF-CMA security (after [BS23], Section 7.4).

                                                      source
                                                      theorem Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeGame_wordProbPadTest {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {query : ℕ → ProbComp (List Bool)} {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k m : List Bool) => BitString.ofList n (hash n k m)) ↑(ε n)) (hε : Negligible ε) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hquery : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits query) (hforge : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool × List Bool) => forge p.1 p.2.1 p.2.2) :
                                                      Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfOneTimeGame (seed n).eval family n (fun (k m : List Bool) => BitString.ofList n (hash n k m)) (Protocols.CarterWegman.OneTimeForger.ofProbComp (query n) fun (m : List Bool) (t : BitString n) => do let p ← forge n m (List.ofFn t) pure (p.1, BitString.ofList n p.2)))

                                                      Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman EUF-CMA security for uniform word-level families (after [BS23], Section 7.4).

                                                      source
                                                      theorem Cslib.Crypto.PseudorandomFunction.negligible_prfOneTimeStrongGame_wordProbPadTest {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {query : ℕ → ProbComp (List Bool)} {forge : ℕ → List Bool → List Bool → ProbComp (List Bool × List Bool)} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k m : List Bool) => BitString.ofList n (hash n k m)) ↑(ε n)) (hε : Negligible ε) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hquery : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits query) (hforge : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (p : ℕ × List Bool × List Bool) => forge p.1 p.2.1 p.2.2) :
                                                      Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfOneTimeStrongGame (seed n).eval family n (fun (k m : List Bool) => BitString.ofList n (hash n k m)) (Protocols.CarterWegman.OneTimeForger.ofProbComp (query n) fun (m : List Bool) (t : BitString n) => do let p ← forge n m (List.ofFn t) pure (p.1, BitString.ofList n p.2)))

                                                      Asymptotic one-query fixed-nonce PRF-masked Carter–Wegman SUF-CMA security for uniform word-level families (after [BS23], Section 7.4).

                                                      Multi-query fresh-nonce PRF-masked Carter–Wegman MAC (after Boneh–Shoup Section 7.5) #

                                                      source
                                                      noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterSeqHandler {K M Y : Type} [AddGroup Y] (hash : K → M → Y) (k : K) (padSeq : ℕ → Y) (m : M) :
                                                      StateT (List (M × Y)) PMF Y

                                                      Counter Carter–Wegman signing handler driven by a deterministic pad sequence padSeq : ℕ → Y: on the i-th query m (i = pads.length), it uses the pad r = padSeq pads.length, appends (m, r) to the pad log, and returns sign hash k r m.

                                                      Instances For
                                                        source
                                                        @[simp]
                                                        theorem Cslib.Crypto.Protocols.CarterWegman.run_counterSeqHandler {K M Y : Type} [AddGroup Y] (hash : K → M → Y) (k : K) (padSeq : ℕ → Y) (m : M) (pads : List (M × Y)) :
                                                        (counterSeqHandler hash k padSeq m).run pads = PMF.pure (sign hash k (padSeq pads.length) m, pads ++ [(m, padSeq pads.length)])
                                                        source
                                                        @[simp]
                                                        theorem Cslib.Crypto.Protocols.CarterWegman.run_counterRealHandler {K M Y : Type} [AddGroup Y] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (m : M) (pads : List (M × Y)) :
                                                        (counterRealHandler hash k m).run pads = (Probability.PMF.uniformOfFintype Y).bind fun (r : Y) => PMF.pure (sign hash k r m, pads ++ [(m, r)])
                                                        source
                                                        theorem Cslib.Crypto.Protocols.CarterWegman.run_interpret_counterSeqHandler_congr {K M Y : Type} [AddGroup Y] {α : Type} (hash : K → M → Y) (k : K) {padSeq₁ padSeq₂ : ℕ → Y} {prog : OracleComp (fun (x : M) => Y) α} {Q : ℕ} (hprog : prog.IsQueryBounded Q) (pads : List (M × Y)) (hpad : ∀ (i : ℕ), pads.length ≤ i → i < pads.length + Q → padSeq₁ i = padSeq₂ i) :
                                                        (OracleComp.interpret (counterSeqHandler hash k padSeq₁) prog).run pads = (OracleComp.interpret (counterSeqHandler hash k padSeq₂) prog).run pads

                                                        If prog makes at most Q queries, then running prog against counterSeqHandler from pads depends only on the pads padSeq i for i ∈ [pads.length, pads.length + Q).

                                                        source
                                                        theorem Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_counterSeqHandler {K M Y : Type} [AddGroup Y] {ι α : Type} [DecidableEq ι] [Fintype ι] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (nonce : ℕ → ι) {prog : OracleComp (fun (x : M) => Y) α} {Q : ℕ} (hprog : prog.IsQueryBounded Q) (pads : List (M × Y)) (hinj : ∀ (i : ℕ), pads.length ≤ i → i < pads.length + Q → ∀ (j : ℕ), pads.length ≤ j → j < pads.length + Q → nonce i = nonce j → i = j) :
                                                        ((Probability.PMF.uniformOfFintype (ι → Y)).bind fun (table : ι → Y) => (OracleComp.interpret (counterSeqHandler hash k fun (i : ℕ) => table (nonce i)) prog).run pads) = (OracleComp.interpret (counterRealHandler hash k) prog).run pads

                                                        When table ← PMF.uniformOfFintype (ι → Y) is a uniformly random function and nonce : ℕ → ι is injective on [pads.length, pads.length + Q), running any Q-query-bounded program prog against counterSeqHandler hash k (fun i => table (nonce i)) from pads has the exact same distribution as running prog against counterRealHandler hash k from pads.

                                                        source
                                                        noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedCounterSlotGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
                                                        PMF Bool

                                                        The issued-slot EUF-CMA experiment for the counter Carter–Wegman MAC under an arbitrary pad-sequence distribution padSeqDist : PMF (ℕ → Y).

                                                        Instances For
                                                          source
                                                          noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedCounterGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
                                                          PMF Bool

                                                          The issued-counter global-message-freshness EUF-CMA experiment under an arbitrary pad-sequence distribution padSeqDist : PMF (ℕ → Y).

                                                          Instances For
                                                            source
                                                            noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedCounterStrongGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
                                                            PMF Bool

                                                            The issued-slot strong SUF-CMA experiment under an arbitrary pad-sequence distribution padSeqDist : PMF (ℕ → Y).

                                                            Instances For
                                                              source
                                                              theorem Cslib.Crypto.Protocols.CarterWegman.maskedCounterStrongGame_eq_maskedCounterSlotGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
                                                              maskedCounterStrongGame seed padSeqDist hash forger = maskedCounterSlotGame seed padSeqDist hash forger
                                                              source
                                                              theorem Cslib.Crypto.Protocols.CarterWegman.maskedCounterGame_le_maskedCounterSlotGame {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
                                                              (maskedCounterGame seed padSeqDist hash forger) true ≤ (maskedCounterSlotGame seed padSeqDist hash forger) true
                                                              source
                                                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.counterPadSeqDistinguisher {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : CounterForger M Y) (padSeq : ℕ → Y) :
                                                              PMF Bool

                                                              The induced multi-query pad-sequence distinguisher (ℕ → Y) → PMF Bool that samples k ← seed and s ← forger.coins, simulates forger.forge s using counterSeqHandler hash k padSeq, and evaluates checkCounterSlot hash k.

                                                              Instances For
                                                                source
                                                                theorem Cslib.Crypto.Protocols.CarterWegman.maskedCounterSlotGame_eq_bind_counterPadSeqDistinguisher {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (padSeqDist : PMF (ℕ → Y)) (hash : K → M → Y) (forger : CounterForger M Y) :
                                                                maskedCounterSlotGame seed padSeqDist hash forger = padSeqDist.bind (counterPadSeqDistinguisher seed hash forger)
                                                                source
                                                                theorem Cslib.Crypto.Protocols.CarterWegman.counterPadSeqDistinguisher_congr {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) {forger : CounterForger M Y} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) {padSeq₁ padSeq₂ : ℕ → Y} (hpad : ∀ i < Q, padSeq₁ i = padSeq₂ i) :
                                                                counterPadSeqDistinguisher seed hash forger padSeq₁ = counterPadSeqDistinguisher seed hash forger padSeq₂

                                                                If forger makes at most Q signing queries, then counterPadSeqDistinguisher depends only on the first Q pads padSeq 0, ..., padSeq (Q - 1).

                                                                source
                                                                theorem Cslib.Crypto.Protocols.CarterWegman.uniform_bind_counterPadSeqDistinguisher {K M Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] {ι : Type} [DecidableEq ι] [Fintype ι] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (nonce : ℕ → ι) {forger : CounterForger M Y} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) (hinj : ∀ i < Q, ∀ j < Q, nonce i = nonce j → i = j) :
                                                                ((Probability.PMF.uniformOfFintype (ι → Y)).bind fun (table : ι → Y) => counterPadSeqDistinguisher seed hash forger fun (i : ℕ) => table (nonce i)) = counterSlotGame seed hash forger

                                                                When table ← PMF.uniformOfFintype (ι → Y) and nonce : ℕ → ι is injective on {0, ..., Q - 1}, sampling table and running counterPadSeqDistinguisher on fun i => table (nonce i) has the exact same distribution as counterSlotGame seed hash forger.

                                                                source
                                                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfPadSeqDist (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool) :
                                                                PMF (ℕ → BitString n)

                                                                The multi-query pad-sequence distribution on ℕ → BitString n obtained by sampling a uniform n-bit PRF key key ← BitString.uniformList n and evaluating prfOracle family n key (nonce i) at each counter index i.

                                                                Instances For
                                                                  source
                                                                  noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfCounterSlotGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
                                                                  PMF Bool

                                                                  The multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot EUF-CMA experiment (after [BS23], Section 7.5, Theorem 7.10), where the signer's counter schedule nonce fixes the nonces and checkCounterSlot accepts only issued counter indices (pads[idx]? = some r), rejecting unissued idx.

                                                                  Instances For
                                                                    source
                                                                    noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfCounterGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
                                                                    PMF Bool

                                                                    The multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA experiment (after [BS23], Section 7.5, Theorem 7.10), where the signer's counter schedule nonce fixes the nonces and checkCounterGlobal accepts only issued counter indices (pads[idx]? = some r), rejecting unissued idx.

                                                                    Instances For
                                                                      source
                                                                      noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfCounterStrongGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
                                                                      PMF Bool

                                                                      The multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot strong SUF-CMA experiment (after [BS23], Section 7.5, Theorem 7.10), where the signer's counter schedule nonce fixes the nonces and checkCounterStrong accepts only issued counter indices (pads[idx]? = some r), rejecting unissued idx.

                                                                      Instances For
                                                                        source
                                                                        theorem Cslib.Crypto.Protocols.CarterWegman.prfCounterStrongGame_eq_prfCounterSlotGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
                                                                        prfCounterStrongGame seed family n nonce hash forger = prfCounterSlotGame seed family n nonce hash forger
                                                                        source
                                                                        theorem Cslib.Crypto.Protocols.CarterWegman.prfCounterGame_le_prfCounterSlotGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (nonce : ℕ → List Bool) (hash : K → M → BitString n) (forger : CounterForger M (BitString n)) :
                                                                        (prfCounterGame seed family n nonce hash forger) true ≤ (prfCounterSlotGame seed family n nonce hash forger) true
                                                                        source
                                                                        def Cslib.Crypto.Protocols.CarterWegman.prfPadCollectStep (n : ℕ) (nonce : ℕ → ℕ → List Bool) (pads : List (List Bool)) :
                                                                        Probability.WordOracleComp Unit (List (List Bool))

                                                                        One step of multi-pad collection at security parameter n under nonce schedule nonce: query the external oracle at nonce n pads.length, take at most n reply bits, and append the reply to pads.

                                                                        Instances For
                                                                          source
                                                                          def Cslib.Crypto.Protocols.CarterWegman.prfMultiPadDistinguisher (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) :
                                                                          OracleDistinguisher

                                                                          Multi-query PRF OracleDistinguisher for a query budget Q : ℕ → ℕ, nonce schedule nonce : ℕ → ℕ → List Bool, and pad-sequence test test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool: at security parameter n, collect Q n oracle replies at nonce n 0, ..., nonce n (Q n - 1) and run test n on the n-bit views of the collected replies.

                                                                          Instances For
                                                                            source
                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfMultiPadDistinguisher {K M : Type} [DecidableEq M] {n : ℕ} (seed : PMF K) (family : List Bool → List Bool → List Bool) (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) (hash : K → M → BitString n) {forger : CounterForger M (BitString n)} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded (Q n)) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest : ∀ (padSeq : ℕ → BitString n), counterPadSeqDistinguisher seed hash forger padSeq = (test n padSeq).eval) :
                                                                            (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n).eval = prfCounterSlotGame seed family n (nonce n) hash forger

                                                                            In prfRealGame, when forger makes at most Q n signing queries and test n realizes counterPadSeqDistinguisher seed hash forger, prfMultiPadDistinguisher Q nonce test has the exact outcome distribution of prfCounterSlotGame seed family n (nonce n) hash forger.

                                                                            source
                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfMultiPadDistinguisher {K M : Type} [DecidableEq M] {n : ℕ} (seed : PMF K) (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) (hash : K → M → BitString n) {forger : CounterForger M (BitString n)} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest : ∀ (padSeq : ℕ → BitString n), counterPadSeqDistinguisher seed hash forger padSeq = (test n padSeq).eval) :
                                                                            (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n).eval = counterSlotGame seed hash forger

                                                                            In prfIdealGame, when forger makes at most Q n signing queries, each nonce n i (i < Q n) has length n, the Q n nonces are pairwise distinct on {0, ..., Q n - 1}, and test n realizes counterPadSeqDistinguisher seed hash forger, prfMultiPadDistinguisher Q nonce test has the exact outcome distribution of the ideal counterSlotGame seed hash forger.

                                                                            source
                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.prfCounterSlotGame_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) {forger : CounterForger M (BitString n)} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest : ∀ (padSeq : ℕ → BitString n), counterPadSeqDistinguisher seed hash forger padSeq = (test n padSeq).eval) :
                                                                            ((prfCounterSlotGame seed family n (nonce n) hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n).eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n).eval)

                                                                            Multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot reduction (after [BS23], Section 7.5, Theorem 7.10): when hash is ε-almost-Δ-universal (ε ≠ ⊤), forger makes at most Q n signing queries, and nonce n 0, ..., nonce n (Q n - 1) are pairwise distinct n-bit nonces fixed by the signer's counter schedule, the real-valued issued-slot forgery probability in prfCounterSlotGame is at most ε.toReal plus the concrete PRF distinguishing advantage of prfMultiPadDistinguisher Q nonce test at parameter n (with unissued counter indices rejected by checkCounterSlot).

                                                                            source
                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.prfCounterGame_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) {forger : CounterForger M (BitString n)} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest : ∀ (padSeq : ℕ → BitString n), counterPadSeqDistinguisher seed hash forger padSeq = (test n padSeq).eval) :
                                                                            ((prfCounterGame seed family n (nonce n) hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n).eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n).eval)

                                                                            Multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA reduction (after [BS23], Section 7.5, Theorem 7.10).

                                                                            source
                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.prfCounterStrongGame_le {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (Q : ℕ → ℕ) (nonce : ℕ → ℕ → List Bool) {forger : CounterForger M (BitString n)} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest : ∀ (padSeq : ℕ → BitString n), counterPadSeqDistinguisher seed hash forger padSeq = (test n padSeq).eval) :
                                                                            ((prfCounterStrongGame seed family n (nonce n) hash forger) true).toReal ≤ ε.toReal + ↑(Game.advantage (prfRealGame family (prfMultiPadDistinguisher Q nonce test) n).eval (prfIdealGame (prfMultiPadDistinguisher Q nonce test) n).eval)

                                                                            Multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot SUF-CMA reduction (after [BS23], Section 7.5, Theorem 7.10).

                                                                            source
                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfMultiPadDistinguisher {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool} {test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool} (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnonce : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => nonce p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool fun (p : ℕ × List (List Bool)) => test p.1 fun (i : ℕ) => BitString.ofList p.1 (p.2.getD i [])) :
                                                                            Probability.IsOraclePPT Turing.MultiTapeTM.encBool (prfMultiPadDistinguisher Q nonce test)

                                                                            prfMultiPadDistinguisher Q nonce test is uniformly strict oracle-PPT (IsOraclePPT encBool) whenever the query budget Q, the nonce schedule nonce, and the pad-list test test are uniformly polynomial-time / strict PPT.

                                                                            source
                                                                            theorem Cslib.Crypto.PseudorandomFunction.negligible_prfCounterSlotGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool} (forger : (n : ℕ) → Protocols.CarterWegman.CounterForger (M n) (BitString n)) (hforger : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : (forger n).Coins), ((forger n).forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest_eval : ∀ (n : ℕ) (padSeq : ℕ → BitString n), Protocols.CarterWegman.counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq = (test n padSeq).eval) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnonce : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => nonce p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) (htest_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool fun (p : ℕ × List (List Bool)) => test p.1 fun (i : ℕ) => BitString.ofList p.1 (p.2.getD i [])) :
                                                                            Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfCounterSlotGame (seed n) family n (nonce n) (hash n) (forger n))

                                                                            Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot security (after [BS23], Section 7.5, Theorem 7.10). The query bound hforger and nonce conditions hnonce_len, hnonce_inj are required only eventually (∀ᶠ n in Filter.atTop), so any polynomial query budget Q n (where Q n ≤ 2 ^ n holds for all sufficiently large n) is covered without patching small n.

                                                                            source
                                                                            theorem Cslib.Crypto.PseudorandomFunction.negligible_prfCounterGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool} (forger : (n : ℕ) → Protocols.CarterWegman.CounterForger (M n) (BitString n)) (hforger : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : (forger n).Coins), ((forger n).forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest_eval : ∀ (n : ℕ) (padSeq : ℕ → BitString n), Protocols.CarterWegman.counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq = (test n padSeq).eval) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnonce : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => nonce p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) (htest_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool fun (p : ℕ × List (List Bool)) => test p.1 fun (i : ℕ) => BitString.ofList p.1 (p.2.getD i [])) :
                                                                            Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfCounterGame (seed n) family n (nonce n) (hash n) (forger n))

                                                                            Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-counter EUF-CMA security (after [BS23], Section 7.5, Theorem 7.10).

                                                                            source
                                                                            theorem Cslib.Crypto.PseudorandomFunction.negligible_prfCounterStrongGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) {Q : ℕ → ℕ} {nonce : ℕ → ℕ → List Bool} (forger : (n : ℕ) → Protocols.CarterWegman.CounterForger (M n) (BitString n)) (hforger : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : (forger n).Coins), ((forger n).forge s).IsQueryBounded (Q n)) (hnonce_len : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < Q n, (nonce n i).length = n) (hnonce_inj : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < Q n, ∀ j < Q n, nonce n i = nonce n j → i = j) (test : (k : ℕ) → (ℕ → BitString k) → ProbComp Bool) (htest_eval : ∀ (n : ℕ) (padSeq : ℕ → BitString n), Protocols.CarterWegman.counterPadSeqDistinguisher (seed n) (hash n) (forger n) padSeq = (test n padSeq).eval) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnonce : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => nonce p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) (htest_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool fun (p : ℕ × List (List Bool)) => test p.1 fun (i : ℕ) => BitString.ofList p.1 (p.2.getD i [])) :
                                                                            Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfCounterStrongGame (seed n) family n (nonce n) (hash n) (forger n))

                                                                            Asymptotic multi-query fresh-nonce PRF-masked Carter–Wegman issued-slot SUF-CMA security (after [BS23], Section 7.5, Theorem 7.10).

                                                                            Full nonce-based Carter–Wegman MAC (Boneh–Shoup Attack Game 7.4 and Theorem 7.10) #

                                                                            source
                                                                            structure Cslib.Crypto.Protocols.CarterWegman.NonceForger (M N Y : Type) :
                                                                            Type 1

                                                                            An adaptive multi-query forger in the nonce-based MAC game ([BS23], Section 7.5.1, Attack Game 7.4, p. 274): it draws private coins s ← coins, makes adaptive signing queries (m, x) : M × N (receiving tag t : Y), and outputs a candidate forgery ((m', x'), t') : (M × N) × Y.

                                                                            • Coins : Type

                                                                              Type of the forger's private coins.

                                                                            • coins : PMF self.Coins

                                                                              Distribution of the forger's private coins.

                                                                            • forge : self.Coins → OracleComp (fun (x : M × N) => Y) ((M × N) × Y)

                                                                              Adaptive oracle program making signing queries (m, x) : M × N and outputting a candidate forgery ((m', x'), t') : (M × N) × Y.

                                                                            Instances For
                                                                              source
                                                                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.nonceFnHandler {K M N Y : Type} [AddGroup Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (q : M × N) :
                                                                              StateT (List ((M × N) × Y)) PMF Y

                                                                              Nonce-based Carter–Wegman signing handler driven by a pad function padFn : N → Y: on signing query q = (m, x), compute t = sign hash k (padFn x) m, append (q, t) to the query–tag transcript tr, and return t.

                                                                              Instances For
                                                                                source
                                                                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.nonceSimHandler {M N Y : Type} [Fintype Y] [Nonempty Y] (q : M × N) :
                                                                                StateT (List ((M × N) × Y)) PMF Y

                                                                                Simulated key-independent nonce signing handler: on query q = (m, x), sample a uniform tag t ← PMF.uniformOfFintype Y, append (q, t) to the query–tag transcript tr, and return t.

                                                                                Instances For
                                                                                  source
                                                                                  def Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) (tr : List ((M × N) × Y)) (table : N → Y) :
                                                                                  N → Y

                                                                                  Reconstruct a pad function N → Y from a query–tag transcript tr : List ((M × N) × Y) and a background table table : N → Y, setting the pad at each queried nonce x_i to -hash k m_i + t_i while retaining table x at all unqueried nonces x.

                                                                                  Instances For
                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_nil {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) (table : N → Y) :
                                                                                    reconstructPadFn hash k [] table = table
                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_cons {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) (e : (M × N) × Y) (tr : List ((M × N) × Y)) (table : N → Y) :
                                                                                    reconstructPadFn hash k (e :: tr) table = reconstructPadFn hash k tr (Function.update table e.1.2 (-hash k e.1.1 + e.2))
                                                                                    source
                                                                                    @[simp]
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_append_singleton {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) (tr : List ((M × N) × Y)) (e : (M × N) × Y) (table : N → Y) :
                                                                                    reconstructPadFn hash k (tr ++ [e]) table = Function.update (reconstructPadFn hash k tr table) e.1.2 (-hash k e.1.1 + e.2)
                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_apply_of_not_mem {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) {tr : List ((M × N) × Y)} {x : N} (hx : x ∉ List.map (fun (e : (M × N) × Y) => e.1.2) tr) (table : N → Y) :
                                                                                    reconstructPadFn hash k tr table x = table x

                                                                                    At any nonce x not appearing in tr, reconstructPadFn hash k tr table x = table x.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_congr_of_forall_ne {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) {tr : List ((M × N) × Y)} {x : N} {table₁ table₂ : N → Y} (h : ∀ (z : N), z ≠ x → table₁ z = table₂ z) (z : N) :
                                                                                    z ≠ x → reconstructPadFn hash k tr table₁ z = reconstructPadFn hash k tr table₂ z

                                                                                    If table₁ and table₂ agree away from x, then so do reconstructPadFn hash k tr table₁ and reconstructPadFn hash k tr table₂.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_append_update_self {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) (tr : List ((M × N) × Y)) (m : M) (x : N) (t r : Y) (table : N → Y) :
                                                                                    reconstructPadFn hash k (tr ++ [((m, x), t)]) (Function.update table x r) = reconstructPadFn hash k (tr ++ [((m, x), t)]) table

                                                                                    Updating table at x before folding tr ++ [((m, x), t)] is overwritten by the final update at x.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_append_sign_of_not_mem {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) {tr : List ((M × N) × Y)} (m : M) {x : N} (hx : x ∉ List.map (fun (e : (M × N) × Y) => e.1.2) tr) (table : N → Y) :
                                                                                    reconstructPadFn hash k (tr ++ [((m, x), sign hash k (table x) m)]) table = reconstructPadFn hash k tr table

                                                                                    When x ∉ tr.map (fun e => e.1.2), appending ((m, x), sign hash k (table x) m) leaves reconstructPadFn hash k tr table unchanged.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.reconstructPadFn_apply_of_mem_of_nodup {K M N Y : Type} [AddGroup Y] [DecidableEq N] (hash : K → M → Y) (k : K) {tr : List ((M × N) × Y)} {e : (M × N) × Y} (he : e ∈ tr) (hnodup : (List.map (fun (e : (M × N) × Y) => e.1.2) tr).Nodup) (table : N → Y) :
                                                                                    reconstructPadFn hash k tr table e.1.2 = -hash k e.1.1 + e.2

                                                                                    For any entry e ∈ tr in a transcript with distinct nonces (tr.map (fun e => e.1.2)).Nodup, reconstructPadFn evaluates at e.1.2 to -hash k e.1.1 + e.2.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.uniform_reconstructPadFn_step {K M N Y : Type} [AddGroup Y] {β : Type} [Fintype N] [DecidableEq N] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) {tr : List ((M × N) × Y)} (m : M) {x : N} (hx : x ∉ List.map (fun (e : (M × N) × Y) => e.1.2) tr) (F : Y → List ((M × N) × Y) → (N → Y) → PMF β) :
                                                                                    ((Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => have t := sign hash k (reconstructPadFn hash k tr table x) m; F t (tr ++ [((m, x), t)]) (reconstructPadFn hash k tr table)) = (Probability.PMF.uniformOfFintype Y).bind fun (t : Y) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => F t (tr ++ [((m, x), t)]) (reconstructPadFn hash k (tr ++ [((m, x), t)]) table)

                                                                                    Single-step pad-to-tag resampling identity for a fresh nonce x ∉ tr.map (fun e => e.1.2): sampling table ← PMF.uniformOfFintype (N → Y) and signing m at x under reconstructPadFn hash k tr table is identical to sampling a uniform tag t ← PMF.uniformOfFintype Y and reconstructing reconstructPadFn hash k (tr ++ [((m, x), t)]) table.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_nonceFnHandler {K M N Y : Type} [AddGroup Y] {α β : Type} [Fintype N] [DecidableEq N] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (prog : OracleComp (fun (x : M × N) => Y) α) (tr : List ((M × N) × Y)) (post : α → List ((M × N) × Y) → (N → Y) → PMF β) (c : PMF β) (hpost : ∀ (a : α) (tr' : List ((M × N) × Y)) (padFn : N → Y), ¬(List.map (fun (e : (M × N) × Y) => e.1.2) tr').Nodup → post a tr' padFn = c) :
                                                                                    ((Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => ((OracleComp.interpret (nonceFnHandler hash k (reconstructPadFn hash k tr table)) prog).run tr).bind fun (res : α × List ((M × N) × Y)) => post res.1 res.2 (reconstructPadFn hash k tr table)) = ((OracleComp.interpret nonceSimHandler prog).run tr).bind fun (res : α × List ((M × N) × Y)) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => post res.1 res.2 (reconstructPadFn hash k res.2 table)

                                                                                    Multi-query simulation equivalence for nonceFnHandler under a random function: for any post-processing post that collapses to a constant distribution c whenever the transcript has a repeated nonce (¬ (tr'.map (fun e => e.1.2)).Nodup), running prog against nonceFnHandler hash k (reconstructPadFn hash k tr table) over table ← PMF.uniformOfFintype (N → Y) has the exact same distribution as running prog against the key-independent nonceSimHandler and reconstructing reconstructPadFn hash k res.2 table at the end.

                                                                                    source
                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.probOracleComp_uniform_bind_run_interpret_nonceFnHandler {K M N Y : Type} [AddGroup Y] {α β : Type} [Fintype N] [DecidableEq N] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (prog : ProbOracleComp (fun (x : M × N) => Y) α) (tr : List ((M × N) × Y)) (post : α → List ((M × N) × Y) → (N → Y) → PMF β) (c : PMF β) (hpost : ∀ (a : α) (tr' : List ((M × N) × Y)) (padFn : N → Y), ¬(List.map (fun (e : (M × N) × Y) => e.1.2) tr').Nodup → post a tr' padFn = c) :
                                                                                    ((Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => ((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 : α × List ((M × N) × Y)) => 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 : α × List ((M × N) × Y)) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => post res.1 res.2 (reconstructPadFn hash k res.2 table)

                                                                                    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) α).

                                                                                    source
                                                                                    def Cslib.Crypto.Protocols.CarterWegman.checkNonceSUF {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                    Bool

                                                                                    Nonce-based SUF-CMA verification predicate on a query–tag transcript tr and pad function padFn ([BS23], Section 7.5.1, Attack Game 7.4, p. 274): all signing queries in tr used distinct nonces ((tr.map (fun e => e.1.2)).Nodup), the candidate out = ((m', x'), t') was not returned by any signing query (!tr.contains out), and verify hash k (padFn x') m' t' = true.

                                                                                    Instances For
                                                                                      source
                                                                                      def Cslib.Crypto.Protocols.CarterWegman.checkNonceEUF {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                      Bool

                                                                                      Nonce-based EUF-CMA (message-freshness) verification predicate on a query–tag transcript tr and pad function padFn: all signing queries in tr used distinct nonces, the message m' = out.1.1 was never queried (!(tr.map (fun e => e.1.1)).contains out.1.1), and verify hash k (padFn x') m' t' = true.

                                                                                      Instances For
                                                                                        source
                                                                                        theorem Cslib.Crypto.Protocols.CarterWegman.checkNonceEUF_imp_checkNonceSUF {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                        checkNonceEUF hash k padFn tr out = true → checkNonceSUF hash k padFn tr out = true

                                                                                        Global message freshness (checkNonceEUF) implies pair freshness (checkNonceSUF).

                                                                                        source
                                                                                        noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedNonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                        PMF Bool

                                                                                        The nonce-based Carter–Wegman SUF-CMA experiment under an arbitrary pad-function distribution rfDist : PMF (N → Y).

                                                                                        Instances For
                                                                                          source
                                                                                          noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedNonceGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                          PMF Bool

                                                                                          The nonce-based Carter–Wegman EUF-CMA (message-freshness) experiment under an arbitrary pad-function distribution rfDist : PMF (N → Y).

                                                                                          Instances For
                                                                                            source
                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.maskedNonceGame_le_maskedNonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                            (maskedNonceGame seed rfDist hash forger) true ≤ (maskedNonceStrongGame seed rfDist hash forger) true

                                                                                            Monotonicity from message-freshness (maskedNonceGame) to triple-freshness (maskedNonceStrongGame).

                                                                                            source
                                                                                            noncomputable def Cslib.Crypto.Protocols.CarterWegman.nonceFnDistinguisher {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (seed : PMF K) (hash : K → M → Y) (forger : NonceForger M N Y) (rf : N → Y) :
                                                                                            PMF Bool

                                                                                            The induced pad-function distinguisher (N → Y) → PMF Bool for maskedNonceStrongGame.

                                                                                            Instances For
                                                                                              source
                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.maskedNonceStrongGame_eq_bind_nonceFnDistinguisher {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                              maskedNonceStrongGame seed rfDist hash forger = rfDist.bind (nonceFnDistinguisher seed hash forger)
                                                                                              source
                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.seed_uniform_checkNonceSUF_le {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                              (seed.bind fun (k : K) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => PMF.pure (checkNonceSUF hash k (reconstructPadFn hash k tr table) tr out)) true ≤ max ε (↑(Fintype.card Y))⁻¹

                                                                                              Under IsDeltaUniversalHash seed hash ε, for any fixed transcript tr and candidate forgery out = ((m', x'), t'), the probability over k ← seed and table ← PMF.uniformOfFintype (N → Y) that checkNonceSUF hash k (reconstructPadFn hash k tr table) tr out = true is at most max ε (Fintype.card Y : ℝ≥0∞)⁻¹: at most ε when x' is an issued nonce in tr, and at most (Fintype.card Y : ℝ≥0∞)⁻¹ when x' is an unissued nonce.

                                                                                              source
                                                                                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                              PMF Bool

                                                                                              The ideal nonce-based Carter–Wegman SUF-CMA experiment ([BS23], Section 7.5.1, Attack Game 7.4 and Theorem 7.10, p. 274) under a truly random function rf ← PMF.uniformOfFintype (N → Y).

                                                                                              Instances For
                                                                                                source
                                                                                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.nonceGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                                PMF Bool

                                                                                                The ideal nonce-based Carter–Wegman EUF-CMA (message-freshness) experiment implied by the SUF game (nonceStrongGame) under a truly random function rf ← PMF.uniformOfFintype (N → Y).

                                                                                                Instances For
                                                                                                  source
                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.nonceGame_le_nonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : NonceForger M N Y) :
                                                                                                  (nonceGame seed hash forger) true ≤ (nonceStrongGame seed hash forger) true

                                                                                                  Monotonicity from the message-freshness variant (nonceGame) to nonceStrongGame.

                                                                                                  source
                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_le_max {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : NonceForger M N Y) :
                                                                                                  (nonceStrongGame seed hash forger) true ≤ max ε (↑(Fintype.card Y))⁻¹

                                                                                                  Ideal nonce-based Carter–Wegman SUF-CMA security (max bound) ([BS23], Section 7.5.1, Theorem 7.10, p. 274): under IsDeltaUniversalHash seed hash ε, every adaptive NonceForger wins nonceStrongGame with probability at most max ε (Fintype.card Y : ℝ≥0∞)⁻¹.

                                                                                                  source
                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_le {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : NonceForger M N Y) :
                                                                                                  (nonceStrongGame seed hash forger) true ≤ ε + (↑(Fintype.card Y))⁻¹

                                                                                                  Ideal nonce-based Carter–Wegman SUF-CMA security (+ bound) ([BS23], Section 7.5.1, Theorem 7.10, p. 274): winning probability is at most ε + (Fintype.card Y : ℝ≥0∞)⁻¹.

                                                                                                  source
                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.nonceGame_le_max {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : NonceForger M N Y) :
                                                                                                  (nonceGame seed hash forger) true ≤ max ε (↑(Fintype.card Y))⁻¹

                                                                                                  Ideal nonce-based Carter–Wegman EUF-CMA (message-freshness) security (max bound).

                                                                                                  source
                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.nonceGame_le {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (forger : NonceForger M N Y) :
                                                                                                  (nonceGame seed hash forger) true ≤ ε + (↑(Fintype.card Y))⁻¹

                                                                                                  Ideal nonce-based Carter–Wegman EUF-CMA (message-freshness) security (+ bound).

                                                                                                  source
                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.maskedNonceStrongGame_toReal_le_add_advantage {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (rfDist : PMF (N → Y)) (forger : NonceForger M N Y) :
                                                                                                  ((maskedNonceStrongGame seed rfDist hash forger) true).toReal ≤ ε.toReal + (↑(Fintype.card Y))⁻¹.toReal + ↑(Game.advantage (rfDist.bind (nonceFnDistinguisher seed hash forger)) ((Probability.PMF.uniformOfFintype (N → Y)).bind (nonceFnDistinguisher seed hash forger)))

                                                                                                  Hybrid bound for maskedNonceStrongGame ([BS23], Section 7.5.1, Theorem 7.10, p. 274): under IsDeltaUniversalHash seed hash ε (ε ≠ ⊤), the real-valued SUF-CMA forgery probability under rfDist is at most ε.toReal + ((Fintype.card Y : ℝ≥0∞)⁻¹).toReal plus the distinguishing advantage of nonceFnDistinguisher between rfDist and PMF.uniformOfFintype (N → Y).

                                                                                                  source
                                                                                                  noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfFnDist (family : List Bool → List Bool → List Bool) (n : ℕ) :
                                                                                                  PMF (BitString n → BitString n)

                                                                                                  The distribution on BitString n → BitString n induced by a uniform n-bit PRF key key ← BitString.uniformList n under prfOracle family n key.

                                                                                                  Instances For
                                                                                                    source
                                                                                                    noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfNonceStrongGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : NonceForger M (BitString n) (BitString n)) :
                                                                                                    PMF Bool

                                                                                                    The PRF-masked nonce-based Carter–Wegman SUF-CMA experiment ([BS23], Section 7.5.1, Attack Game 7.4 and Theorem 7.10, p. 274).

                                                                                                    Instances For
                                                                                                      source
                                                                                                      noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfNonceGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : NonceForger M (BitString n) (BitString n)) :
                                                                                                      PMF Bool

                                                                                                      The PRF-masked nonce-based Carter–Wegman EUF-CMA (message-freshness) experiment implied by prfNonceStrongGame.

                                                                                                      Instances For
                                                                                                        source
                                                                                                        theorem Cslib.Crypto.Protocols.CarterWegman.prfNonceStrongGame_le_of_distinguisher {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : NonceForger M (BitString n) (BitString n)) (D : OracleDistinguisher) (hreal : (prfRealGame family D n).eval = (prfFnDist family n).bind (nonceFnDistinguisher seed hash forger)) (hideal : (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (nonceFnDistinguisher seed hash forger)) :
                                                                                                        ((prfNonceStrongGame seed family n hash forger) true).toReal ≤ ε.toReal + (2 ^ n)⁻¹ + ↑(Game.advantage (prfRealGame family D n).eval (prfIdealGame D n).eval)

                                                                                                        Nonce-based Carter–Wegman SUF-CMA reduction ([BS23], Section 7.5.1, Theorem 7.10, p. 274): if D simulates nonceFnDistinguisher seed hash forger in prfRealGame and prfIdealGame, then the real-valued SUF-CMA forgery probability in prfNonceStrongGame is bounded by ε.toReal + (2 ^ n)⁻¹ plus the PRF distinguishing advantage of D.

                                                                                                        source
                                                                                                        theorem Cslib.Crypto.Protocols.CarterWegman.prfNonceGame_le_of_distinguisher {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) (forger : NonceForger M (BitString n) (BitString n)) (D : OracleDistinguisher) (hreal : (prfRealGame family D n).eval = (prfFnDist family n).bind (nonceFnDistinguisher seed hash forger)) (hideal : (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (nonceFnDistinguisher seed hash forger)) :
                                                                                                        ((prfNonceGame seed family n hash forger) true).toReal ≤ ε.toReal + (2 ^ n)⁻¹ + ↑(Game.advantage (prfRealGame family D n).eval (prfIdealGame D n).eval)

                                                                                                        Nonce-based Carter–Wegman EUF-CMA (message-freshness) reduction implied by prfNonceStrongGame_le_of_distinguisher.

                                                                                                        source
                                                                                                        theorem Cslib.Crypto.PseudorandomFunction.negligible_prfNonceStrongGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) (forger : (n : ℕ) → Protocols.CarterWegman.NonceForger (M n) (BitString n) (BitString n)) (D : OracleDistinguisher) (hD : Probability.IsOraclePPT Turing.MultiTapeTM.encBool D) (hreal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfRealGame family D n).eval = (Protocols.CarterWegman.prfFnDist family n).bind (Protocols.CarterWegman.nonceFnDistinguisher (seed n) (hash n) (forger n))) (hideal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (Protocols.CarterWegman.nonceFnDistinguisher (seed n) (hash n) (forger n))) :
                                                                                                        Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfNonceStrongGame (seed n) family n (hash n) (forger n))

                                                                                                        Asymptotic nonce-based Carter–Wegman SUF-CMA security ([BS23], Section 7.5.1, Theorem 7.10, p. 274): given an OracleDistinguisher D satisfying IsOraclePPT encBool D together with hypotheses hreal and hideal asserting that D simulates nonceFnDistinguisher (seed n) (hash n) (forger n) in prfRealGame and prfIdealGame (forger itself carries no efficiency assumption), prfNonceStrongGame has negligible success probability under PseudorandomFunction family and a statistical IsDeltaUniversalHash family with negligible ε.

                                                                                                        source
                                                                                                        theorem Cslib.Crypto.PseudorandomFunction.negligible_prfNonceGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) (forger : (n : ℕ) → Protocols.CarterWegman.NonceForger (M n) (BitString n) (BitString n)) (D : OracleDistinguisher) (hD : Probability.IsOraclePPT Turing.MultiTapeTM.encBool D) (hreal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfRealGame family D n).eval = (Protocols.CarterWegman.prfFnDist family n).bind (Protocols.CarterWegman.nonceFnDistinguisher (seed n) (hash n) (forger n))) (hideal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (Protocols.CarterWegman.nonceFnDistinguisher (seed n) (hash n) (forger n))) :
                                                                                                        Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfNonceGame (seed n) family n (hash n) (forger n))

                                                                                                        Asymptotic nonce-based Carter–Wegman EUF-CMA (message-freshness) security implied by negligible_prfNonceStrongGame; as there, D, hreal, and hideal assume the PRF reduction wrapper while forger carries no efficiency assumption.

                                                                                                        source
                                                                                                        noncomputable def Cslib.Crypto.Protocols.CarterWegman.carterWegmanNonceMAC (msgLen : ℕ → ℕ) (seed : ℕ → ProbComp (List Bool)) (hash : ℕ → List Bool → List Bool → List Bool) (family : List Bool → List Bool → List Bool) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
                                                                                                        NonceMACScheme

                                                                                                        Computational nonce-based Carter–Wegman MAC (NonceMACScheme) ([BS23], 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 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.
                                                                                                        Instances For
                                                                                                          source
                                                                                                          def Cslib.Crypto.Protocols.CarterWegman.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)) (Probability.WordOracleComp Unit) (List Bool)

                                                                                                          Open stateful handler for the nonce-based Carter–Wegman PRF reduction ([BS23], 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.

                                                                                                          Instances For
                                                                                                            source
                                                                                                            def Cslib.Crypto.Protocols.CarterWegman.prfNonceToPrfDistinguisher (msgLen : ℕ → ℕ) (seed : ℕ → ProbComp (List Bool)) (hash : ℕ → List Bool → List Bool → List Bool) (adversary : NonceMACForger) :
                                                                                                            OracleDistinguisher

                                                                                                            Oracle reduction turning an adaptive word-level NonceMACForger into an OracleDistinguisher for the PRF security game ([BS23], 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.
                                                                                                            Instances For
                                                                                                              source
                                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfNonceToPrfDistinguisher {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {adversary : NonceMACForger} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) adversary) :
                                                                                                              Probability.IsOraclePPT Turing.MultiTapeTM.encBool (prfNonceToPrfDistinguisher msgLen seed hash adversary)

                                                                                                              prfNonceToPrfDistinguisher is uniformly strict oracle-PPT (IsOraclePPT encBool) whenever msgLen, seed, hash, and adversary are uniformly polynomial-time / strict PPT.

                                                                                                              source
                                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfNonceToPrfDistinguisher {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {family : List Bool → List Bool → List Bool} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (adversary : NonceMACForger) (n : ℕ) :
                                                                                                              (prfRealGame family (prfNonceToPrfDistinguisher msgLen seed hash adversary) n).eval = ((carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame adversary n).eval

                                                                                                              Running prfNonceToPrfDistinguisher msgLen seed hash adversary in prfRealGame family produces the exact same Boolean distribution as (carterWegmanNonceMAC ...).sufCmaGame adversary n.

                                                                                                              source
                                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfNonceToPrfDistinguisher_le {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {n : ℕ} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) (adversary : NonceMACForger) :
                                                                                                              (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n).eval true ≤ max ε (2 ^ n)⁻¹

                                                                                                              Ideal-game bound for prfNonceToPrfDistinguisher ([BS23], 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)⁻¹.

                                                                                                              source
                                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_carterWegmanNonceMAC_toReal_le {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {family : List Bool → List Bool → List Bool} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {n : ℕ} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) (hε : ε ≠ ⊤) (adversary : NonceMACForger) :
                                                                                                              (((carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame adversary n).eval true).toReal ≤ ε.toReal + (2 ^ n)⁻¹ + ↑(Game.advantage (prfRealGame family (prfNonceToPrfDistinguisher msgLen seed hash adversary) n).eval (prfIdealGame (prfNonceToPrfDistinguisher msgLen seed hash adversary) n).eval)

                                                                                                              Quantitative SUF-CMA bound for carterWegmanNonceMAC ([BS23], 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.

                                                                                                              source
                                                                                                              theorem 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 : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ↑(ε n)) (hε : Negligible ε) :
                                                                                                              (Protocols.CarterWegman.carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash ⋯).SUFCMA

                                                                                                              Asymptotic NonceMACScheme.SUFCMA security of carterWegmanNonceMAC ([BS23], 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.

                                                                                                              source
                                                                                                              theorem 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 : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ↑(ε n)) (hε : Negligible ε) :
                                                                                                              (Protocols.CarterWegman.carterWegmanNonceMAC msgLen seed hash family hmsgLen hseed hhash ⋯).EUFCMA

                                                                                                              Asymptotic NonceMACScheme.EUFCMA security of carterWegmanNonceMAC ([BS23], Section 7.5.1, Theorem 7.10, p. 274).

                                                                                                              Randomized Carter–Wegman MAC (Boneh–Shoup Section 7.4, Theorem 7.9) #

                                                                                                              source
                                                                                                              structure Cslib.Crypto.Protocols.CarterWegman.RandomNonceForger (M N Y : Type) :
                                                                                                              Type 1

                                                                                                              An adaptive multi-query forger against the randomized Carter–Wegman MAC ([BS23], Section 7.4, Theorem 7.9, p. 270): it draws private coins s ← coins, makes adaptive signing queries m : M (receiving (x, t) : N × Y where x is a random nonce chosen by the signer), and outputs a candidate forgery ((m', x'), t') : (M × N) × Y.

                                                                                                              • Coins : Type

                                                                                                                Type of the forger's private coins.

                                                                                                              • coins : PMF self.Coins

                                                                                                                Distribution of the forger's private coins.

                                                                                                              • forge : self.Coins → OracleComp (fun (x : M) => N × Y) ((M × N) × Y)

                                                                                                                Adaptive oracle program making signing queries m : M and outputting a candidate forgery ((m', x'), t') : (M × N) × Y.

                                                                                                              Instances For
                                                                                                                source
                                                                                                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.randomNonceFnHandler {K M N Y : Type} [AddGroup Y] [Fintype N] [Nonempty N] (hash : K → M → Y) (k : K) (padFn : N → Y) (m : M) :
                                                                                                                StateT (List ((M × N) × Y)) PMF (N × Y)

                                                                                                                Randomized Carter–Wegman signing handler driven by a pad function padFn : N → Y ([BS23], Section 7.4, p. 267): on signing query m, sample a uniform nonce x ← PMF.uniformOfFintype N, compute t = sign hash k (padFn x) m, append ((m, x), t) to the transcript tr, and return (x, t).

                                                                                                                Instances For
                                                                                                                  source
                                                                                                                  noncomputable def Cslib.Crypto.Protocols.CarterWegman.randomNonceSimHandler {M N Y : Type} [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] (m : M) :
                                                                                                                  StateT (List ((M × N) × Y)) PMF (N × Y)

                                                                                                                  Simulated key-independent randomized signing handler: on query m, sample independent uniform (x, t) ← PMF.uniformOfFintype N × PMF.uniformOfFintype Y, append ((m, x), t) to tr, and return (x, t).

                                                                                                                  Instances For
                                                                                                                    source
                                                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.uniform_bind_run_interpret_randomNonceFnHandler {K M N Y : Type} [AddGroup Y] {α β : Type} [Fintype N] [Nonempty N] [DecidableEq N] [Fintype Y] [Nonempty Y] (hash : K → M → Y) (k : K) (prog : OracleComp (fun (x : M) => N × Y) α) (tr : List ((M × N) × Y)) (post : α → List ((M × N) × Y) → (N → Y) → PMF β) (c : PMF β) (hpost : ∀ (a : α) (tr' : List ((M × N) × Y)) (padFn : N → Y), ¬(List.map (fun (e : (M × N) × Y) => e.1.2) tr').Nodup → post a tr' padFn = c) :
                                                                                                                    ((Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => ((OracleComp.interpret (randomNonceFnHandler hash k (reconstructPadFn hash k tr table)) prog).run tr).bind fun (res : α × List ((M × N) × Y)) => post res.1 res.2 (reconstructPadFn hash k tr table)) = ((OracleComp.interpret randomNonceSimHandler prog).run tr).bind fun (res : α × List ((M × N) × Y)) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => post res.1 res.2 (reconstructPadFn hash k res.2 table)

                                                                                                                    Multi-query simulation equivalence for randomNonceFnHandler under a random function: for any post-processing post that collapses to a constant distribution c whenever the transcript has a repeated nonce (¬ (tr'.map (fun e => e.1.2)).Nodup), running prog against randomNonceFnHandler hash k (reconstructPadFn hash k tr table) over table ← PMF.uniformOfFintype (N → Y) has the exact same distribution as running prog against randomNonceSimHandler and reconstructing reconstructPadFn hash k res.2 table at the end.

                                                                                                                    source
                                                                                                                    theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceSimHandler_not_nodup_le {M N Y α : Type} [Fintype N] [Nonempty N] [DecidableEq N] [Fintype Y] [Nonempty Y] {prog : OracleComp (fun (x : M) => N × Y) α} {Q : ℕ} (hprog : prog.IsQueryBounded Q) (tr : List ((M × N) × Y)) :
                                                                                                                    (((OracleComp.interpret randomNonceSimHandler prog).run tr).bind fun (res : α × List ((M × N) × Y)) => PMF.pure !decide (List.map (fun (e : (M × N) × Y) => e.1.2) res.2).Nodup) true ≤ if (List.map (fun (e : (M × N) × Y) => e.1.2) tr).Nodup then ↑(∑ i ∈ Finset.range Q, (tr.length + i)) / ↑(Fintype.card N) else 1

                                                                                                                    Birthday-collision bound for randomNonceSimHandler: starting from tr, any Q-query-bounded 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.

                                                                                                                    source
                                                                                                                    def Cslib.Crypto.Protocols.CarterWegman.checkRandomNonceSUF {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                                                    Bool

                                                                                                                    Randomized Carter–Wegman SUF-CMA verification predicate ([BS23], Section 7.4, Theorem 7.9, p. 270): the candidate out = ((m', x'), t') was not returned by any signing query (!tr.contains out) and verify hash k (padFn x') m' t' = true.

                                                                                                                    Instances For
                                                                                                                      source
                                                                                                                      def Cslib.Crypto.Protocols.CarterWegman.checkRandomNonceEUF {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                                                      Bool

                                                                                                                      Randomized Carter–Wegman EUF-CMA (message-freshness) verification predicate: the message m' = out.1.1 was never queried (!(tr.map (fun e => e.1.1)).contains out.1.1) and verify hash k (padFn x') m' t' = true.

                                                                                                                      Instances For
                                                                                                                        source
                                                                                                                        theorem Cslib.Crypto.Protocols.CarterWegman.checkRandomNonceEUF_imp_checkRandomNonceSUF {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] (hash : K → M → Y) (k : K) (padFn : N → Y) (tr : List ((M × N) × Y)) (out : (M × N) × Y) :
                                                                                                                        checkRandomNonceEUF hash k padFn tr out = true → checkRandomNonceSUF hash k padFn tr out = true

                                                                                                                        Randomized Carter–Wegman EUF-CMA implies SUF-CMA (checkRandomNonceSUF), since a fresh message m' cannot appear in any issued transcript triple ((mᵢ, xᵢ), tᵢ) ∈ tr.

                                                                                                                        source
                                                                                                                        noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedRandomNonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                        PMF Bool

                                                                                                                        The randomized Carter–Wegman SUF-CMA experiment under an arbitrary pad-function distribution rfDist : PMF (N → Y).

                                                                                                                        Instances For
                                                                                                                          source
                                                                                                                          noncomputable def Cslib.Crypto.Protocols.CarterWegman.maskedRandomNonceGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq Y] [Fintype N] [Nonempty N] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                          PMF Bool

                                                                                                                          The randomized Carter–Wegman EUF-CMA (message-freshness) experiment under an arbitrary pad-function distribution rfDist : PMF (N → Y).

                                                                                                                          Instances For
                                                                                                                            source
                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.maskedRandomNonceGame_le_maskedRandomNonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                            (maskedRandomNonceGame seed rfDist hash forger) true ≤ (maskedRandomNonceStrongGame seed rfDist hash forger) true

                                                                                                                            In maskedRandomNonceGame, message-freshness forgery probability is bounded by strong unforgeability (maskedRandomNonceStrongGame).

                                                                                                                            source
                                                                                                                            noncomputable def Cslib.Crypto.Protocols.CarterWegman.randomNonceFnDistinguisher {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] (seed : PMF K) (hash : K → M → Y) (forger : RandomNonceForger M N Y) (rf : N → Y) :
                                                                                                                            PMF Bool

                                                                                                                            The induced pad-function distinguisher (N → Y) → PMF Bool for maskedRandomNonceStrongGame.

                                                                                                                            Instances For
                                                                                                                              source
                                                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.maskedRandomNonceStrongGame_eq_bind_randomNonceFnDistinguisher {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] (seed : PMF K) (rfDist : PMF (N → Y)) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                              maskedRandomNonceStrongGame seed rfDist hash forger = rfDist.bind (randomNonceFnDistinguisher seed hash forger)

                                                                                                                              Factoring maskedRandomNonceStrongGame through randomNonceFnDistinguisher.

                                                                                                                              source
                                                                                                                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                              PMF Bool

                                                                                                                              The ideal randomized Carter–Wegman SUF-CMA experiment ([BS23], Section 7.4, Theorem 7.9, p. 270) under a truly random function rf ← PMF.uniformOfFintype (N → Y).

                                                                                                                              Instances For
                                                                                                                                source
                                                                                                                                noncomputable def Cslib.Crypto.Protocols.CarterWegman.randomNonceGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                                PMF Bool

                                                                                                                                The ideal randomized Carter–Wegman EUF-CMA (message-freshness) experiment under a truly random function rf ← PMF.uniformOfFintype (N → Y).

                                                                                                                                Instances For
                                                                                                                                  source
                                                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceGame_le_randomNonceStrongGame {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] (seed : PMF K) (hash : K → M → Y) (forger : RandomNonceForger M N Y) :
                                                                                                                                  (randomNonceGame seed hash forger) true ≤ (randomNonceStrongGame seed hash forger) true

                                                                                                                                  In randomNonceGame, message-freshness forgery probability is bounded by strong unforgeability (randomNonceStrongGame).

                                                                                                                                  source
                                                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_le_sum_add_max {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) {forger : RandomNonceForger M N Y} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) :
                                                                                                                                  (randomNonceStrongGame seed hash forger) true ≤ ↑(∑ i ∈ Finset.range Q, i) / ↑(Fintype.card N) + max ε (↑(Fintype.card Y))⁻¹

                                                                                                                                  Ideal randomized Carter–Wegman SUF-CMA security (∑ i < Q + max bound) ([BS23], Section 7.4, Theorem 7.9, p. 270): under IsDeltaUniversalHash seed hash ε, any Q-query-bounded RandomNonceForger wins randomNonceStrongGame with probability at most ((∑ i ∈ Finset.range Q, i : ℕ) : ℝ≥0∞) / Fintype.card N + max ε (Fintype.card Y : ℝ≥0∞)⁻¹.

                                                                                                                                  source
                                                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_le {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) {forger : RandomNonceForger M N Y} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) :
                                                                                                                                  (randomNonceStrongGame seed hash forger) true ≤ ↑Q ^ 2 / (2 * ↑(Fintype.card N)) + (↑(Fintype.card Y))⁻¹ + ε

                                                                                                                                  Ideal randomized Carter–Wegman SUF-CMA security ([BS23], Section 7.4, Theorem 7.9, p. 270): under IsDeltaUniversalHash seed hash ε, any Q-query-bounded RandomNonceForger wins randomNonceStrongGame with probability at most (Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) + (Fintype.card Y : ℝ≥0∞)⁻¹ + ε.

                                                                                                                                  source
                                                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceGame_le {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) {forger : RandomNonceForger M N Y} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) :
                                                                                                                                  (randomNonceGame seed hash forger) true ≤ ↑Q ^ 2 / (2 * ↑(Fintype.card N)) + (↑(Fintype.card Y))⁻¹ + ε

                                                                                                                                  Ideal randomized Carter–Wegman EUF-CMA (message-freshness) security ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                  source
                                                                                                                                  theorem Cslib.Crypto.Protocols.CarterWegman.maskedRandomNonceStrongGame_toReal_le_add_advantage {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (rfDist : PMF (N → Y)) {forger : RandomNonceForger M N Y} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) :
                                                                                                                                  ((maskedRandomNonceStrongGame seed rfDist hash forger) true).toReal ≤ (↑Q ^ 2 / (2 * ↑(Fintype.card N))).toReal + (↑(Fintype.card Y))⁻¹.toReal + ε.toReal + ↑(Game.advantage (rfDist.bind (randomNonceFnDistinguisher seed hash forger)) ((Probability.PMF.uniformOfFintype (N → Y)).bind (randomNonceFnDistinguisher seed hash forger)))

                                                                                                                                  Hybrid bound for maskedRandomNonceStrongGame ([BS23], Section 7.4, Theorem 7.9, p. 270): under IsDeltaUniversalHash seed hash ε (ε ≠ ⊤), any Q-query-bounded RandomNonceForger wins maskedRandomNonceStrongGame with real-valued probability at most ((Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N)).toReal + ((Fintype.card Y : ℝ≥0∞)⁻¹).toReal + ε.toReal plus the distinguishing advantage of randomNonceFnDistinguisher.

                                                                                                                                  source
                                                                                                                                  noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceStrongGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : RandomNonceForger M (BitString n) (BitString n)) :
                                                                                                                                  PMF Bool

                                                                                                                                  The PRF-masked randomized Carter–Wegman SUF-CMA experiment ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                  Instances For
                                                                                                                                    source
                                                                                                                                    noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceGame {K M : Type} [DecidableEq M] (seed : PMF K) (family : List Bool → List Bool → List Bool) (n : ℕ) (hash : K → M → BitString n) (forger : RandomNonceForger M (BitString n) (BitString n)) :
                                                                                                                                    PMF Bool

                                                                                                                                    The PRF-masked randomized Carter–Wegman EUF-CMA (message-freshness) experiment ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                    Instances For
                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceStrongGame_le_of_distinguisher {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) {forger : RandomNonceForger M (BitString n) (BitString n)} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) (D : OracleDistinguisher) (hreal : (prfRealGame family D n).eval = (prfFnDist family n).bind (randomNonceFnDistinguisher seed hash forger)) (hideal : (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (randomNonceFnDistinguisher seed hash forger)) :
                                                                                                                                      ((prfRandomNonceStrongGame seed family n hash forger) true).toReal ≤ ↑Q ^ 2 / (2 * 2 ^ n) + (2 ^ n)⁻¹ + ε.toReal + ↑(Game.advantage (prfRealGame family D n).eval (prfIdealGame D n).eval)

                                                                                                                                      Randomized Carter–Wegman SUF-CMA reduction ([BS23], Section 7.4, Theorem 7.9, p. 270): if D simulates randomNonceFnDistinguisher seed hash forger in prfRealGame and prfIdealGame, then any Q-query-bounded RandomNonceForger wins prfRandomNonceStrongGame with real-valued probability at most (Q : ℝ) ^ 2 / (2 * 2 ^ n) + (2 ^ n)⁻¹ + ε.toReal plus the PRF distinguishing advantage of D.

                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceGame_le_of_distinguisher {K M : Type} [DecidableEq M] {n : ℕ} {seed : PMF K} {hash : K → M → BitString n} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) (hε : ε ≠ ⊤) (family : List Bool → List Bool → List Bool) {forger : RandomNonceForger M (BitString n) (BitString n)} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) (D : OracleDistinguisher) (hreal : (prfRealGame family D n).eval = (prfFnDist family n).bind (randomNonceFnDistinguisher seed hash forger)) (hideal : (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (randomNonceFnDistinguisher seed hash forger)) :
                                                                                                                                      ((prfRandomNonceGame seed family n hash forger) true).toReal ≤ ↑Q ^ 2 / (2 * 2 ^ n) + (2 ^ n)⁻¹ + ε.toReal + ↑(Game.advantage (prfRealGame family D n).eval (prfIdealGame D n).eval)

                                                                                                                                      Randomized Carter–Wegman EUF-CMA (message-freshness) reduction ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.PseudorandomFunction.negligible_prfRandomNonceStrongGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) {Q : ℕ → ℕ} (hQ : PolynomiallyBounded Q) (forger : (n : ℕ) → Protocols.CarterWegman.RandomNonceForger (M n) (BitString n) (BitString n)) (hforger : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : (forger n).Coins), ((forger n).forge s).IsQueryBounded (Q n)) (D : OracleDistinguisher) (hD : Probability.IsOraclePPT Turing.MultiTapeTM.encBool D) (hreal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfRealGame family D n).eval = (Protocols.CarterWegman.prfFnDist family n).bind (Protocols.CarterWegman.randomNonceFnDistinguisher (seed n) (hash n) (forger n))) (hideal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (Protocols.CarterWegman.randomNonceFnDistinguisher (seed n) (hash n) (forger n))) :
                                                                                                                                      Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfRandomNonceStrongGame (seed n) family n (hash n) (forger n))

                                                                                                                                      Asymptotic randomized Carter–Wegman SUF-CMA security ([BS23], Section 7.4, Theorem 7.9, p. 270): if family is a PseudorandomFunction, hash n is a family of ε n-difference-universal hashes into BitString n with Negligible ε, forger n is bounded by Q n queries with PolynomiallyBounded Q, and D is an IsOraclePPT encBool distinguisher that simulates randomNonceFnDistinguisher in prfRealGame (hreal) and prfIdealGame (hideal), then the SUF-CMA success probability Game.succProbability (prfRandomNonceStrongGame ...) is Negligible. Note that this theorem assumes the PRF reduction wrapper D and its simulation contracts hreal/hideal as hypotheses (whilst forger carries only the query bound hforger and no efficiency certificate).

                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.PseudorandomFunction.negligible_prfRandomNonceGame {K M : ℕ → Type} [(n : ℕ) → DecidableEq (M n)] {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) {seed : (n : ℕ) → PMF (K n)} {hash : (n : ℕ) → K n → M n → BitString n} {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n) (hash n) ↑(ε n)) (hε : Negligible ε) {Q : ℕ → ℕ} (hQ : PolynomiallyBounded Q) (forger : (n : ℕ) → Protocols.CarterWegman.RandomNonceForger (M n) (BitString n) (BitString n)) (hforger : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (s : (forger n).Coins), ((forger n).forge s).IsQueryBounded (Q n)) (D : OracleDistinguisher) (hD : Probability.IsOraclePPT Turing.MultiTapeTM.encBool D) (hreal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfRealGame family D n).eval = (Protocols.CarterWegman.prfFnDist family n).bind (Protocols.CarterWegman.randomNonceFnDistinguisher (seed n) (hash n) (forger n))) (hideal : ∀ᶠ (n : ℕ) in Filter.atTop, (prfIdealGame D n).eval = (Probability.PMF.uniformOfFintype (BitString n → BitString n)).bind (Protocols.CarterWegman.randomNonceFnDistinguisher (seed n) (hash n) (forger n))) :
                                                                                                                                      Negligible fun (n : ℕ) => Game.succProbability (Protocols.CarterWegman.prfRandomNonceGame (seed n) family n (hash n) (forger n))

                                                                                                                                      Asymptotic randomized Carter–Wegman EUF-CMA (message-freshness) security ([BS23], Section 7.4, Theorem 7.9, p. 270), assuming the IsOraclePPT encBool PRF reduction wrapper D and its simulation contracts hreal/hideal.

                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.Protocols.CarterWegman.probOracleComp_uniform_bind_run_interpret_randomNonceFnHandler {K M N Y : Type} [AddGroup Y] [DecidableEq N] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {α β : Type} (hash : K → M → Y) (k : K) (prog : ProbOracleComp (fun (x : M) => N × Y) α) (tr : List ((M × N) × Y)) (post : α → List ((M × N) × Y) → (N → Y) → PMF β) (c : PMF β) (hpost : ∀ (a : α) (tr' : List ((M × N) × Y)) (padFn : N → Y), ¬(List.map (fun (e : (M × N) × Y) => e.1.2) tr').Nodup → post a tr' padFn = c) :
                                                                                                                                      ((Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => ((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 : α × List ((M × N) × Y)) => 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 : α × List ((M × N) × Y)) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (table : N → Y) => post res.1 res.2 (reconstructPadFn hash k res.2 table)

                                                                                                                                      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.

                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.Protocols.CarterWegman.probOracleComp_randomNonceSimHandler_not_nodup_le {M N Y : Type} [DecidableEq N] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {α : Type} {prog : ProbOracleComp (fun (x : 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 : α × List ((M × N) × Y)) => PMF.pure !decide (List.map (fun (e : (M × N) × Y) => e.1.2) res.2).Nodup) true ≤ if (List.map (fun (e : (M × N) × Y) => e.1.2) tr).Nodup then ↑(∑ i ∈ Finset.range Q, (tr.length + i)) / ↑(Fintype.card N) else 1

                                                                                                                                      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.

                                                                                                                                      source
                                                                                                                                      theorem Cslib.Crypto.Protocols.CarterWegman.seed_uniform_probOracleComp_checkRandomNonceSUF_le {K M N Y : Type} [AddGroup Y] [DecidableEq M] [DecidableEq N] [DecidableEq Y] [Fintype N] [Nonempty N] [Fintype Y] [Nonempty Y] {α : Type} {seed : PMF K} {hash : K → M → Y} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash seed hash ε) {prog : ProbOracleComp (fun (x : M) => N × Y) α} {Q : ℕ} (hprog : prog.IsQueryBounded Q) (out : α → (M × N) × Y) :
                                                                                                                                      (seed.bind fun (k : K) => (Probability.PMF.uniformOfFintype (N → Y)).bind fun (rf : N → Y) => ((OracleComp.interpret (ProbOracleComp.handler (fun (m : ℕ) => StateT.lift (ProbComp.unifOracle m)) (randomNonceFnHandler hash k rf)) prog).run []).bind fun (res : α × List ((M × N) × Y)) => PMF.pure (checkRandomNonceSUF hash k rf res.2 (out res.1))) true ≤ ↑Q ^ 2 / (2 * ↑(Fintype.card N)) + (↑(Fintype.card Y))⁻¹ + ε

                                                                                                                                      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∞)⁻¹ + ε.

                                                                                                                                      Word-level MACScheme packaging and IsOraclePPT PRF reduction (Theorem 7.9) #

                                                                                                                                      source
                                                                                                                                      noncomputable def Cslib.Crypto.Protocols.CarterWegman.carterWegmanRandomMAC (msgLen : ℕ → ℕ) (seed : ℕ → ProbComp (List Bool)) (hash : ℕ → List Bool → List Bool → List Bool) (family : List Bool → List Bool → List Bool) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
                                                                                                                                      MACScheme

                                                                                                                                      Computational randomized Carter–Wegman MAC (MACScheme) ([BS23], 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.
                                                                                                                                      Instances For
                                                                                                                                        source
                                                                                                                                        noncomputable def Cslib.Crypto.Protocols.CarterWegman.cwRandomNonceLogHandler (msgLen : ℕ → ℕ) (hash : ℕ → List Bool → List Bool → List Bool) (n : ℕ) (k : List Bool) (request : Unit × List Bool) :
                                                                                                                                        StateT (List (List Bool × List Bool)) (Probability.WordOracleComp Unit) (List Bool)

                                                                                                                                        Open stateful handler for the randomized Carter–Wegman PRF reduction ([BS23], 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.

                                                                                                                                        Instances For
                                                                                                                                          source
                                                                                                                                          noncomputable def Cslib.Crypto.Protocols.CarterWegman.prfRandomNonceToPrfDistinguisher (msgLen : ℕ → ℕ) (seed : ℕ → ProbComp (List Bool)) (hash : ℕ → List Bool → List Bool → List Bool) (adversary : Forger) :
                                                                                                                                          OracleDistinguisher

                                                                                                                                          Oracle reduction turning an adaptive word-level Forger into an OracleDistinguisher for the PRF security game ([BS23], 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.
                                                                                                                                          Instances For
                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.isOraclePPT_prfRandomNonceToPrfDistinguisher {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {adversary : Forger} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                                                                                                                                            Probability.IsOraclePPT Turing.MultiTapeTM.encBool (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary)

                                                                                                                                            prfRandomNonceToPrfDistinguisher is uniformly strict oracle-PPT (IsOraclePPT encBool) whenever msgLen, seed, hash, and adversary are uniformly polynomial-time / strict PPT.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfRealGame_prfRandomNonceToPrfDistinguisher {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {family : List Bool → List Bool → List Bool} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (adversary : Forger) (n : ℕ) :
                                                                                                                                            (prfRealGame family (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n).eval = ((carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame adversary n).eval

                                                                                                                                            Real-game simulation for prfRandomNonceToPrfDistinguisher ([BS23], 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.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.eval_prfIdealGame_prfRandomNonceToPrfDistinguisher_le {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {n Q : ℕ} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) {adversary : Forger} (hq : ProbOracleComp.IsQueryBounded (adversary n []) Q) :
                                                                                                                                            (prfIdealGame (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n).eval true ≤ ↑Q ^ 2 / (2 * 2 ^ n) + (2 ^ n)⁻¹ + ε

                                                                                                                                            Ideal-game bound for prfRandomNonceToPrfDistinguisher ([BS23], 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)⁻¹ + ε.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_carterWegmanRandomMAC_toReal_le {msgLen : ℕ → ℕ} {seed : ℕ → ProbComp (List Bool)} {hash : ℕ → List Bool → List Bool → List Bool} {family : List Bool → List Bool → List Bool} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {n Q : ℕ} {ε : ENNReal} (hh : Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ε) (hε : ε ≠ ⊤) {adversary : Forger} (hq : ProbOracleComp.IsQueryBounded (adversary n []) Q) :
                                                                                                                                            (((carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash hfamily).sufCmaGame adversary n).eval true).toReal ≤ ↑Q ^ 2 / (2 * 2 ^ n) + (2 ^ n)⁻¹ + ε.toReal + ↑(Game.advantage (prfRealGame family (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n).eval (prfIdealGame (prfRandomNonceToPrfDistinguisher msgLen seed hash adversary) n).eval)

                                                                                                                                            Quantitative SUF-CMA bound for carterWegmanRandomMAC ([BS23], 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.

                                                                                                                                            source
                                                                                                                                            theorem 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 : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ↑(ε n)) (hε : Negligible ε) :
                                                                                                                                            (Protocols.CarterWegman.carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash ⋯).SUFCMA

                                                                                                                                            Asymptotic MACScheme.SUFCMA security of carterWegmanRandomMAC ([BS23], 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.

                                                                                                                                            source
                                                                                                                                            theorem 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 : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ↑(ε n)) (hε : Negligible ε) :
                                                                                                                                            (Protocols.CarterWegman.carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash ⋯).EUFCMA

                                                                                                                                            Asymptotic MACScheme.EUFCMA security of carterWegmanRandomMAC ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                            source
                                                                                                                                            theorem 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 : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hseed : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits seed) (hhash : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => hash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits) {ε : ℕ → NNReal} (hh : ∀ (n : ℕ), Probability.IsDeltaUniversalHash (seed n).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (hash n k (List.ofFn m))) ↑(ε n)) (hε : Negligible ε) :
                                                                                                                                            (Protocols.CarterWegman.carterWegmanRandomMAC msgLen seed hash family hmsgLen hseed hhash ⋯).OneTimeEUFCMA

                                                                                                                                            Asymptotic MACScheme.OneTimeEUFCMA security of carterWegmanRandomMAC ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                            Concrete Carter–Wegman instantiations #

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_xpolyHash_le {F : Type} [Field F] [Fintype F] [DecidableEq F] (ℓ : ℕ) (forger : OneTimeForger { m : List F // m.length ≤ ℓ } F) :
                                                                                                                                            (oneTimeGame (Probability.PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => Probability.xpolyHash k ↑m) forger) true ≤ (↑ℓ + 1) / ↑(Fintype.card F)

                                                                                                                                            Polynomial Carter–Wegman one-time MAC (xpolyHash) ([BS23], Section 7.4.1): over a finite field F, authenticating messages of length at most ℓ via xpolyHash has adaptive one-time EUF-CMA (and SUF-CMA) forgery probability at most (ℓ + 1) / |F|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.counterGame_xpolyHash_le {F : Type} [Field F] [Fintype F] [DecidableEq F] (ℓ : ℕ) (forger : CounterForger { m : List F // m.length ≤ ℓ } F) :
                                                                                                                                            (counterGame (Probability.PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => Probability.xpolyHash k ↑m) forger) true ≤ (↑ℓ + 1) / ↑(Fintype.card F)

                                                                                                                                            Polynomial Carter–Wegman multi-query issued-counter MAC (xpolyHash): authenticating messages of length at most ℓ via xpolyHash with fresh pads per query has adaptive multi-query issued-counter EUF-CMA forgery probability at most (ℓ + 1) / |F|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.counterStrongGame_xpolyHash_le {F : Type} [Field F] [Fintype F] [DecidableEq F] (ℓ : ℕ) (forger : CounterForger { m : List F // m.length ≤ ℓ } F) :
                                                                                                                                            (counterStrongGame (Probability.PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => Probability.xpolyHash k ↑m) forger) true ≤ (↑ℓ + 1) / ↑(Fintype.card F)

                                                                                                                                            Polynomial Carter–Wegman multi-query issued-slot strong unforgeability (xpolyHash).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_linearHash_le (n m : ℕ) (forger : OneTimeForger (BitString n) (BitString m)) :
                                                                                                                                            (oneTimeGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger) true ≤ (2 ^ m)⁻¹

                                                                                                                                            Boolean-matrix Carter–Wegman one-time MAC (BitString.LinearHash.hash): hashing n-bit messages to m-bit tags with a uniform Boolean matrix has adaptive one-time forgery probability at most 2⁻ᵐ.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.counterGame_linearHash_le (n m : ℕ) (forger : CounterForger (BitString n) (BitString m)) :
                                                                                                                                            (counterGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger) true ≤ (2 ^ m)⁻¹

                                                                                                                                            Boolean-matrix Carter–Wegman multi-query issued-counter MAC (BitString.LinearHash.hash): adaptive multi-query issued-counter EUF-CMA forgery probability is at most 2⁻ᵐ.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.counterStrongGame_linearHash_le (n m : ℕ) (forger : CounterForger (BitString n) (BitString m)) :
                                                                                                                                            (counterStrongGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger) true ≤ (2 ^ m)⁻¹

                                                                                                                                            Boolean-matrix Carter–Wegman multi-query issued-slot strong unforgeability (BitString.LinearHash.hash).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.prfOneTimeGame_linearHash_le (n m : ℕ) (family : List Bool → List Bool → List Bool) (forger : OneTimeForger (BitString n) (BitString m)) (test : (k : ℕ) → BitString k → ProbComp Bool) (htest : ∀ (r : BitString m), padDistinguisher (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger r = (test m r).eval) :
                                                                                                                                            ((prfOneTimeGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) family m BitString.LinearHash.hash forger) true).toReal ≤ (2 ^ m)⁻¹ + ↑(Game.advantage (prfRealGame family (prfPadDistinguisher test) m).eval (prfIdealGame (prfPadDistinguisher test) m).eval)

                                                                                                                                            Exact single-query PRF-pad reduction for Boolean-matrix Carter–Wegman (BitString.LinearHash.hash) in the one-query, fixed-nonce case (after [BS23], Section 7.4): hashing n-bit messages to m-bit tags with a uniform Boolean matrix and masking by a fixed-nonce PRF evaluation at security parameter m has real-valued one-time forgery probability at most (2 ^ m)⁻¹ plus the concrete PRF distinguishing advantage of prfPadDistinguisher test at parameter m (without asserting IsOraclePPT encBool admissibility or an asymptotic PseudorandomFunction corollary).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_subsetSum_le {ι G : Type} [Fintype ι] [DecidableEq ι] [AddCommGroup G] [Fintype G] [DecidableEq G] (forger : OneTimeForger (ι → Bool) G) :
                                                                                                                                            (oneTimeGame (Probability.PMF.uniformOfFintype (ι → G)) BitString.SubsetSum.hash forger) true ≤ (↑(Fintype.card G))⁻¹

                                                                                                                                            Subset-sum Carter–Wegman one-time MAC (BitString.LinearHash / BitString.SubsetSum.hash): hashing binary words ι → Bool into a finite additive abelian group G via uniform subset-sum weights has adaptive one-time forgery probability at most 1 / |G|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.counterGame_subsetSum_le {ι G : Type} [Fintype ι] [DecidableEq ι] [AddCommGroup G] [Fintype G] [DecidableEq G] (forger : CounterForger (ι → Bool) G) :
                                                                                                                                            (counterGame (Probability.PMF.uniformOfFintype (ι → G)) BitString.SubsetSum.hash forger) true ≤ (↑(Fintype.card G))⁻¹

                                                                                                                                            Subset-sum Carter–Wegman multi-query issued-counter MAC (BitString.SubsetSum.hash): adaptive multi-query issued-counter EUF-CMA forgery probability is at most 1 / |G|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.oneTimeGame_of_isPairwiseIndependentHash_le {K M Y : Type} [Fintype K] [Nonempty K] [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] {hash : K → M → Y} (hh : Probability.IsPairwiseIndependentHash hash) (forger : OneTimeForger M Y) :
                                                                                                                                            (oneTimeGame (Probability.PMF.uniformOfFintype K) hash forger) true ≤ (↑(Fintype.card Y))⁻¹

                                                                                                                                            Pairwise-independent Carter–Wegman one-time MAC: any pairwise independent hash family hash : K → M → Y into a finite additive group Y has adaptive one-time forgery probability at most 1 / |Y|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.counterGame_of_isPairwiseIndependentHash_le {K M Y : Type} [Fintype K] [Nonempty K] [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] {hash : K → M → Y} (hh : Probability.IsPairwiseIndependentHash hash) (forger : CounterForger M Y) :
                                                                                                                                            (counterGame (Probability.PMF.uniformOfFintype K) hash forger) true ≤ (↑(Fintype.card Y))⁻¹

                                                                                                                                            Pairwise-independent Carter–Wegman multi-query issued-counter MAC: any pairwise independent hash family hash : K → M → Y has adaptive multi-query issued-counter forgery probability at most 1 / |Y|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_xpolyHash_le {F N : Type} [Field F] [Fintype F] [DecidableEq F] [Fintype N] [DecidableEq N] (ℓ : ℕ) (forger : NonceForger { m : List F // m.length ≤ ℓ } N F) :
                                                                                                                                            (nonceStrongGame (Probability.PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => Probability.xpolyHash k ↑m) forger) true ≤ (↑ℓ + 1) / ↑(Fintype.card F)

                                                                                                                                            Polynomial Carter–Wegman nonce-based MAC (xpolyHash) ([BS23], Section 7.4.1 and Section 7.5.1, Theorem 7.10, p. 274): over a finite field F and finite nonce space N, authenticating messages of length at most ℓ via xpolyHash has adaptive nonce-based SUF-CMA forgery probability at most (ℓ + 1) / |F| (since 1 / |F| ≤ (ℓ + 1) / |F|).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.nonceGame_xpolyHash_le {F N : Type} [Field F] [Fintype F] [DecidableEq F] [Fintype N] [DecidableEq N] (ℓ : ℕ) (forger : NonceForger { m : List F // m.length ≤ ℓ } N F) :
                                                                                                                                            (nonceGame (Probability.PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => Probability.xpolyHash k ↑m) forger) true ≤ (↑ℓ + 1) / ↑(Fintype.card F)

                                                                                                                                            Polynomial Carter–Wegman nonce-based EUF-CMA (message-freshness) security (xpolyHash).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_xpolyHash_le {F N : Type} [Field F] [Fintype F] [DecidableEq F] [Fintype N] [Nonempty N] [DecidableEq N] (ℓ : ℕ) {forger : RandomNonceForger { m : List F // m.length ≤ ℓ } N F} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) :
                                                                                                                                            (randomNonceStrongGame (Probability.PMF.uniformOfFintype F) (fun (k : F) (m : { m : List F // m.length ≤ ℓ }) => Probability.xpolyHash k ↑m) forger) true ≤ ↑Q ^ 2 / (2 * ↑(Fintype.card N)) + (↑(Fintype.card F))⁻¹ + (↑ℓ + 1) / ↑(Fintype.card F)

                                                                                                                                            Polynomial Carter–Wegman randomized MAC (xpolyHash) ([BS23], Section 7.4, Theorem 7.9, p. 270): over a finite field F and nonempty finite nonce space N, any Q-query-bounded RandomNonceForger wins randomNonceStrongGame with probability at most (Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) + (Fintype.card F : ℝ≥0∞)⁻¹ + (ℓ + 1) / Fintype.card F.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_linearHash_le {N : Type} [Fintype N] [DecidableEq N] (n m : ℕ) (forger : NonceForger (BitString n) N (BitString m)) :
                                                                                                                                            (nonceStrongGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger) true ≤ (2 ^ m)⁻¹

                                                                                                                                            Boolean-matrix Carter–Wegman nonce-based MAC (BitString.LinearHash.hash): hashing n-bit messages to m-bit tags with a uniform Boolean matrix has adaptive nonce-based SUF-CMA forgery probability at most 2⁻ᵐ (since max (2⁻ᵐ) (2⁻ᵐ) = 2⁻ᵐ).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.nonceGame_linearHash_le {N : Type} [Fintype N] [DecidableEq N] (n m : ℕ) (forger : NonceForger (BitString n) N (BitString m)) :
                                                                                                                                            (nonceGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger) true ≤ (2 ^ m)⁻¹

                                                                                                                                            Boolean-matrix Carter–Wegman nonce-based EUF-CMA (message-freshness) security (BitString.LinearHash.hash).

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.randomNonceStrongGame_linearHash_le {N : Type} [Fintype N] [Nonempty N] [DecidableEq N] (n m : ℕ) {forger : RandomNonceForger (BitString n) N (BitString m)} {Q : ℕ} (hforger : ∀ (s : forger.Coins), (forger.forge s).IsQueryBounded Q) :
                                                                                                                                            (randomNonceStrongGame (Probability.PMF.uniformOfFintype (Fin m → BitString n)) BitString.LinearHash.hash forger) true ≤ ↑Q ^ 2 / (2 * ↑(Fintype.card N)) + (2 ^ m)⁻¹ + (2 ^ m)⁻¹

                                                                                                                                            Boolean-matrix Carter–Wegman randomized MAC (BitString.LinearHash.hash) ([BS23], Section 7.4, Theorem 7.9, p. 270): any Q-query-bounded RandomNonceForger wins randomNonceStrongGame with probability at most (Q : ℝ≥0∞) ^ 2 / (2 * Fintype.card N) + ((2 : ℝ≥0∞) ^ m)⁻¹ + ((2 : ℝ≥0∞) ^ m)⁻¹.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_subsetSum_le {ι N G : Type} [Fintype ι] [DecidableEq ι] [Fintype N] [DecidableEq N] [AddCommGroup G] [Fintype G] [DecidableEq G] (forger : NonceForger (ι → Bool) N G) :
                                                                                                                                            (nonceStrongGame (Probability.PMF.uniformOfFintype (ι → G)) BitString.SubsetSum.hash forger) true ≤ (↑(Fintype.card G))⁻¹

                                                                                                                                            Subset-sum Carter–Wegman nonce-based MAC (BitString.SubsetSum.hash): adaptive nonce-based SUF-CMA forgery probability is at most 1 / |G|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.nonceStrongGame_of_isPairwiseIndependentHash_le {K M N Y : Type} [Fintype K] [Nonempty K] [Fintype N] [DecidableEq N] [AddGroup Y] [Fintype Y] [Nonempty Y] [DecidableEq M] [DecidableEq Y] {hash : K → M → Y} (hh : Probability.IsPairwiseIndependentHash hash) (forger : NonceForger M N Y) :
                                                                                                                                            (nonceStrongGame (Probability.PMF.uniformOfFintype K) hash forger) true ≤ (↑(Fintype.card Y))⁻¹

                                                                                                                                            Pairwise-independent Carter–Wegman nonce-based MAC: any pairwise independent hash family hash : K → M → Y has adaptive nonce-based SUF-CMA forgery probability at most 1 / |Y|.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.isPPTOn_linearHashSeed {msgLen : ℕ → ℕ} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :
                                                                                                                                            Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits fun (n : ℕ) => BitString.sampleList (n * msgLen n)

                                                                                                                                            Sampling an (n * msgLen n)-bit Boolean-matrix seed is uniformly strict PPT whenever msgLen is computable in polynomial time.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.computableInPolyTime_linearHashWordHash :
                                                                                                                                            Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List Bool × List Bool) => BitString.LinearHash.wordHash p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits

                                                                                                                                            Uncurried BitString.LinearHash.wordHash is computable in plain polynomial time.

                                                                                                                                            source
                                                                                                                                            theorem Cslib.Crypto.Protocols.CarterWegman.isDeltaUniversalHash_linearHashWordHash (msgLen : ℕ → ℕ) (n : ℕ) :
                                                                                                                                            Probability.IsDeltaUniversalHash (BitString.sampleList (n * msgLen n)).eval (fun (k : List Bool) (m : BitString (msgLen n)) => BitString.ofList n (BitString.LinearHash.wordHash n k (List.ofFn m))) (2 ^ n)⁻¹

                                                                                                                                            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).

                                                                                                                                            source
                                                                                                                                            noncomputable def Cslib.Crypto.Protocols.CarterWegman.linearHashNonceMAC (msgLen : ℕ → ℕ) (family : List Bool → List Bool → List Bool) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
                                                                                                                                            NonceMACScheme

                                                                                                                                            Concrete computational nonce-based Carter–Wegman MAC (NonceMACScheme) from Boolean-matrix linear hashing (BitString.LinearHash.wordHash) and a PRF family family ([BS23], Section 7.5.1, Theorem 7.10, p. 274).

                                                                                                                                            Instances For
                                                                                                                                              source
                                                                                                                                              theorem Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_linearHashNonceMAC_toReal_le {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (n : ℕ) (adversary : NonceMACForger) :
                                                                                                                                              (((linearHashNonceMAC msgLen family hmsgLen hfamily).sufCmaGame adversary n).eval true).toReal ≤ (2 ^ n)⁻¹ + (2 ^ n)⁻¹ + ↑(Game.advantage (prfRealGame family (prfNonceToPrfDistinguisher msgLen (fun (k : ℕ) => BitString.sampleList (k * msgLen k)) BitString.LinearHash.wordHash adversary) n).eval (prfIdealGame (prfNonceToPrfDistinguisher msgLen (fun (k : ℕ) => BitString.sampleList (k * msgLen k)) BitString.LinearHash.wordHash adversary) n).eval)

                                                                                                                                              Quantitative SUF-CMA bound for linearHashNonceMAC ([BS23], 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.

                                                                                                                                              source
                                                                                                                                              theorem Cslib.Crypto.PseudorandomFunction.sufCma_linearHashNonceMAC {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :
                                                                                                                                              (Protocols.CarterWegman.linearHashNonceMAC msgLen family hmsgLen ⋯).SUFCMA

                                                                                                                                              Asymptotic NonceMACScheme.SUFCMA security of linearHashNonceMAC ([BS23], Section 7.5.1, Theorem 7.10, p. 274): for any PseudorandomFunction family and polynomial-time message-length schedule msgLen, linearHashNonceMAC satisfies NonceMACScheme.SUFCMA.

                                                                                                                                              source
                                                                                                                                              theorem Cslib.Crypto.PseudorandomFunction.eufCma_linearHashNonceMAC {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :
                                                                                                                                              (Protocols.CarterWegman.linearHashNonceMAC msgLen family hmsgLen ⋯).EUFCMA

                                                                                                                                              Asymptotic NonceMACScheme.EUFCMA security of linearHashNonceMAC ([BS23], Section 7.5.1, Theorem 7.10, p. 274).

                                                                                                                                              source
                                                                                                                                              noncomputable def Cslib.Crypto.Protocols.CarterWegman.linearHashRandomMAC (msgLen : ℕ → ℕ) (family : List Bool → List Bool → List Bool) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
                                                                                                                                              MACScheme

                                                                                                                                              Concrete computational randomized Carter–Wegman MAC (MACScheme) from Boolean-matrix linear hashing (BitString.LinearHash.wordHash) and a PRF family family ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                              Instances For
                                                                                                                                                source
                                                                                                                                                theorem Cslib.Crypto.Protocols.CarterWegman.sufCmaGame_linearHashRandomMAC_toReal_le {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hfamily : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool) => family p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) {n Q : ℕ} {adversary : Forger} (hq : ProbOracleComp.IsQueryBounded (adversary n []) Q) :
                                                                                                                                                (((linearHashRandomMAC msgLen family hmsgLen hfamily).sufCmaGame adversary n).eval true).toReal ≤ ↑Q ^ 2 / (2 * 2 ^ n) + (2 ^ n)⁻¹ + (2 ^ n)⁻¹ + ↑(Game.advantage (prfRealGame family (prfRandomNonceToPrfDistinguisher msgLen (fun (k : ℕ) => BitString.sampleList (k * msgLen k)) BitString.LinearHash.wordHash adversary) n).eval (prfIdealGame (prfRandomNonceToPrfDistinguisher msgLen (fun (k : ℕ) => BitString.sampleList (k * msgLen k)) BitString.LinearHash.wordHash adversary) n).eval)

                                                                                                                                                Quantitative SUF-CMA bound for linearHashRandomMAC ([BS23], 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.

                                                                                                                                                source
                                                                                                                                                theorem Cslib.Crypto.PseudorandomFunction.sufCma_linearHashRandomMAC {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :
                                                                                                                                                (Protocols.CarterWegman.linearHashRandomMAC msgLen family hmsgLen ⋯).SUFCMA

                                                                                                                                                Asymptotic MACScheme.SUFCMA security of linearHashRandomMAC ([BS23], Section 7.4, Theorem 7.9, p. 270): for any PseudorandomFunction family and polynomial-time message-length schedule msgLen, linearHashRandomMAC satisfies MACScheme.SUFCMA.

                                                                                                                                                source
                                                                                                                                                theorem Cslib.Crypto.PseudorandomFunction.eufCma_linearHashRandomMAC {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :
                                                                                                                                                (Protocols.CarterWegman.linearHashRandomMAC msgLen family hmsgLen ⋯).EUFCMA

                                                                                                                                                Asymptotic MACScheme.EUFCMA security of linearHashRandomMAC ([BS23], Section 7.4, Theorem 7.9, p. 270).

                                                                                                                                                source
                                                                                                                                                theorem Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_linearHashRandomMAC {msgLen : ℕ → ℕ} {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) (hmsgLen : Turing.MultiTapeTM.ComputableInPolyTime msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) :
                                                                                                                                                (Protocols.CarterWegman.linearHashRandomMAC msgLen family hmsgLen ⋯).OneTimeEUFCMA

                                                                                                                                                Asymptotic MACScheme.OneTimeEUFCMA security of linearHashRandomMAC ([BS23], Section 7.4, Theorem 7.9, p. 270).