Documentation

Complexity.Crypto.Computational.MAC

Uniform message authentication codes and PRF-based MACs #

A uniform symmetric message authentication code (MACScheme) consists of a strict probabilistic polynomial-time key generator keyGen, a strict probabilistic polynomial-time tag generator sign, and a deterministic polynomial-time tag verifier verify that accepts every tag produced by sign on an n-bit message under a secret key sampled at security parameter n. Unlike digital signatures (SignatureScheme), verification uses the same secret key as tag generation, and the adversary receives no public key.

We formalize both strong (fresh-pair) existential unforgeability under adaptive chosen-message attack (sufCmaGame, SUFCMA) as in Boneh and Shoup, Attack Game 6.1 / Definition 6.2, and ordinary fresh-message existential unforgeability under adaptive chosen-message attack (eufCmaGame, EUFCMA) and under one-time adaptive chosen-message attack (eufOneTimeGame, OneTimeEUFCMA) against uniform strict oracle-PPT forgers (IsOraclePPT). Both adaptive games share the pair-logging execution core signingPairOracle: sufCmaGame records returned (msg, tag) pairs and accepts any valid n-bit forgery pair (msg, tag) that was never returned (!queriedPairs.contains (msg, tag)), even on a previously queried message, whereas eufCmaGame rejects any candidate forgery whose message was previously queried (!queried.contains msg). We prove the quantitative bound $$\Pr[\text{EUF-CMA}] \le \Pr[\text{SUF-CMA}]$$ (succProbability_eufCmaGame_le_sufCmaGame) and the security implication SUFCMA → EUFCMA (SUFCMA.eufCma). For randomized MACScheme.sign algorithms the two notions differ; for MACs with a unique valid tag per (sk, msg) (eval_sufCmaGame_eq_eufCmaGame_of_unique_tag, sufCma_iff_eufCma_of_unique_tag), including prfMAC, fresh-message and fresh-pair unforgeability coincide.

We then prove that any uniform PseudorandomFunction yields a SUFCMA- and EUFCMA-secure deterministic MAC (prfMAC, PseudorandomFunction.sufCma_prfMAC, PseudorandomFunction.eufCma_prfMAC), with the quantitative security reduction of Boneh and Shoup, Section 6.3, Theorem 6.2: $$\Pr[\text{Forge}] \le \mathrm{Adv}_{\mathrm{PRF}}(B(\mathcal{A}), n) + 2^{-n}.$$

Main definitions #

Main results #

References #

source
structure Cslib.Crypto.MACScheme :
Type

A uniform symmetric message authentication code (MAC) on n-bit messages at security parameter n, with strict polynomial-time key generation and tag generation, deterministic polynomial-time verification, and perfect completeness on supported keys, n-bit messages, and tags Boneh and Shoup, Definition 6.1.

Instances For

    Full adaptive chosen-message security (EUFCMA) #

    source
    noncomputable def Cslib.Crypto.MACScheme.signingOracle (M : MACScheme) (sk : List Bool) (request : Unit × List Bool) :
    StateT (List (List Bool)) ProbComp (List Bool)

    Stateful MAC tagging oracle that tags the requested message under sk and prepends the message to the list of queried messages.

    Instances For
      source
      noncomputable def Cslib.Crypto.MACScheme.eufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
      ProbComp Bool

      The fresh-message MAC EUF-CMA experiment: sample sk ← M.keyGen n, run the adaptive forger on (n, []) with oracle access to M.signingOracle sk, and accept when the forger outputs a valid (msg, tag) pair on an n-bit message msg that was never queried to the tagging oracle.

      Unlike Boneh and Shoup, Attack Game 6.1 / Definition 6.2, which logs (msg, tag) pairs and rejects only previously returned pairs, this experiment logs queried messages and rejects any previously queried message (!out.2.contains out.1.1). The two notions differ for randomized sign algorithms, and coincide for deterministic canonical MACs such as prfMAC.

      Instances For
        source
        theorem Cslib.Crypto.MACScheme.isPPTOn_eufCmaGame (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
        Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (M.eufCmaGame adversary)

        Run the complete MAC EUF-CMA experiment on its unary security parameter for any oracle-PPT forger.

        source
        theorem Cslib.Crypto.MACScheme.isPPT_eufCmaGame (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
        Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => M.eufCmaGame adversary n

        The MAC EUF-CMA experiment is uniformly strict PPT, independently of unused auxiliary input.

        source
        def Cslib.Crypto.MACScheme.EUFCMA (M : MACScheme) :
        Prop

        Fresh-message existential unforgeability under adaptive chosen-message attack (EUFCMA) for a symmetric MAC against uniform strict oracle-PPT adversaries.

        Note that eufCmaGame enforces fresh-message unforgeability (msg ∉ queried), whereas Boneh and Shoup, Attack Game 6.1 / Definition 6.2 defines the stronger fresh-pair variant ((msg, tag) ∉ queriedPairs) for general (possibly randomized) signing algorithms.

        Instances For
          source
          theorem Cslib.Crypto.MACScheme.EUFCMA.negligible {M : MACScheme} (h : M.EUFCMA) (adversary : Forger) (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
          Negligible fun (n : ℕ) => Game.succProbability (M.eufCmaGame adversary n).eval

          Full EUF-CMA security gives negligible forgery probability for every oracle-PPT forger.

          source
          theorem Cslib.Crypto.MACScheme.EUFCMA.of_negligible {M : MACScheme} (h : ∀ (adversary : ℕ → List Bool → Probability.WordOracleComp Unit (List Bool × List Bool)), Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary → Negligible fun (n : ℕ) => Game.succProbability (M.eufCmaGame adversary n).eval) :
          M.EUFCMA

          Establish EUF-CMA security by bounding every oracle-PPT forger's success probability.

          One-time adaptive chosen-message security (OneTimeEUFCMA) #

          source
          noncomputable def Cslib.Crypto.MACScheme.oneTimeSigningOracle (M : MACScheme) (sk : List Bool) (request : Unit × List Bool) :
          StateT (List (List Bool)) ProbComp (List Bool)

          One-time MAC oracle that answers at most the first tagging query using M.sign sk and returns the empty word without tagging on any subsequent query.

          Instances For
            source
            noncomputable def Cslib.Crypto.MACScheme.eufOneTimeGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
            ProbComp Bool

            The one-time MAC EUF-CMA experiment: sample sk ← M.keyGen n, run the adaptive forger on (n, []) with oracle access to M.oneTimeSigningOracle sk, and accept when the forger outputs a valid tag on an n-bit message distinct from the queried message (if any).

            Instances For
              source
              theorem Cslib.Crypto.MACScheme.isPPTOn_run_oneTimeSigningOracle (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
              Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) fun (caller : ℕ × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningOracle caller.2)) (adversary caller.1 [])).run []

              Running an oracle-PPT forger against oneTimeSigningOracle is uniformly strict PPT in the unary security parameter and secret key.

              source
              theorem Cslib.Crypto.MACScheme.isPPTOn_eufOneTimeGame (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
              Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (M.eufOneTimeGame adversary)

              Run the complete one-time MAC EUF-CMA experiment on its unary security parameter for any oracle-PPT forger.

              source
              theorem Cslib.Crypto.MACScheme.isPPT_eufOneTimeGame (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
              Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => M.eufOneTimeGame adversary n

              The one-time MAC EUF-CMA experiment is uniformly strict PPT, independently of unused auxiliary input.

              source
              def Cslib.Crypto.MACScheme.OneTimeEUFCMA (M : MACScheme) :
              Prop

              Existential unforgeability under one-time adaptive chosen-message attack for a symmetric MAC.

              Instances For
                source
                theorem Cslib.Crypto.MACScheme.OneTimeEUFCMA.negligible {M : MACScheme} (h : M.OneTimeEUFCMA) (adversary : Forger) (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                Negligible fun (n : ℕ) => Game.succProbability (M.eufOneTimeGame adversary n).eval

                One-time EUF-CMA security gives negligible forgery probability for every oracle-PPT forger.

                source
                theorem Cslib.Crypto.MACScheme.OneTimeEUFCMA.of_negligible {M : MACScheme} (h : ∀ (adversary : ℕ → List Bool → Probability.WordOracleComp Unit (List Bool × List Bool)), Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary → Negligible fun (n : ℕ) => Game.succProbability (M.eufOneTimeGame adversary n).eval) :
                M.OneTimeEUFCMA

                Establish one-time EUF-CMA security by bounding every oracle-PPT forger's success probability.

                source
                theorem Cslib.Crypto.MACScheme.EUFCMA.oneTimeEUFCMA {M : MACScheme} (h : M.EUFCMA) :
                M.OneTimeEUFCMA

                Full EUF-CMA security implies one-time EUF-CMA security for any MACScheme.

                Strong adaptive chosen-message security (SUFCMA, Boneh–Shoup Attack Game 6.1) #

                source
                noncomputable def Cslib.Crypto.MACScheme.signingPairOracle (M : MACScheme) (sk : List Bool) (request : Unit × List Bool) :
                StateT (List (List Bool × List Bool)) ProbComp (List Bool)

                Stateful MAC tagging oracle that tags the requested message under sk and prepends the returned (msg, tag) pair to the transcript of queried message/tag pairs (Boneh and Shoup, Attack Game 6.1).

                Instances For
                  source
                  noncomputable def Cslib.Crypto.MACScheme.sufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
                  ProbComp Bool

                  The strong (fresh-pair) MAC SUF-CMA experiment (Boneh and Shoup, Attack Game 6.1 / Definition 6.2): sample sk ← M.keyGen n, run the adaptive forger on (n, []) with oracle access to M.signingPairOracle sk, and accept when the forger outputs a valid (msg, tag) pair on an n-bit message msg such that (msg, tag) was never returned by the tagging oracle (!out.2.contains out.1).

                  Instances For
                    source
                    theorem Cslib.Crypto.MACScheme.isPPTOn_run_signingPairOracle (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                    Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) fun (caller : ℕ × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle caller.2)) (adversary caller.1 [])).run []

                    Running an oracle-PPT forger against signingPairOracle is uniformly strict PPT in the unary security parameter and secret key.

                    source
                    theorem Cslib.Crypto.MACScheme.isPPTOn_sufCmaGame (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                    Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (M.sufCmaGame adversary)

                    Run the complete MAC SUF-CMA experiment on its unary security parameter for any oracle-PPT forger.

                    source
                    theorem Cslib.Crypto.MACScheme.isPPT_sufCmaGame (M : MACScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                    Probability.IsPPT Turing.MultiTapeTM.encBool fun (n : ℕ) (x : List Bool) => M.sufCmaGame adversary n

                    The MAC SUF-CMA experiment is uniformly strict PPT, independently of unused auxiliary input.

                    source
                    def Cslib.Crypto.MACScheme.SUFCMA (M : MACScheme) :
                    Prop

                    Strong (fresh-pair) existential unforgeability under adaptive chosen-message attack (SUFCMA) for a symmetric MAC against uniform strict oracle-PPT adversaries (Boneh and Shoup, Attack Game 6.1 / Definition 6.2).

                    Instances For
                      source
                      theorem Cslib.Crypto.MACScheme.SUFCMA.negligible {M : MACScheme} (h : M.SUFCMA) (adversary : Forger) (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                      Negligible fun (n : ℕ) => Game.succProbability (M.sufCmaGame adversary n).eval

                      Strong unforgeability gives negligible SUF-CMA forgery probability for every oracle-PPT forger.

                      source
                      theorem Cslib.Crypto.MACScheme.SUFCMA.of_negligible {M : MACScheme} (h : ∀ (adversary : ℕ → List Bool → Probability.WordOracleComp Unit (List Bool × List Bool)), Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary → Negligible fun (n : ℕ) => Game.succProbability (M.sufCmaGame adversary n).eval) :
                      M.SUFCMA

                      Establish SUF-CMA security by bounding every oracle-PPT forger's success probability.

                      source
                      theorem Cslib.Crypto.MACScheme.eval_run_signingOracle_eq_map_fst_signingPairOracle (M : MACScheme) (sk : List Bool) (prog : Probability.WordOracleComp Unit (List Bool × List Bool)) :
                      ((OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (M.signingOracle sk)) prog).run []).eval = PMF.map (fun (x : (List Bool × List Bool) × List (List Bool × List Bool)) => match x with | (a, s') => (a, List.map Prod.fst s')) ((OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) prog).run []).eval

                      Running an adaptive program against signingOracle produces the exact same distribution as running it against signingPairOracle and projecting the pair transcript to its queried messages.

                      source
                      theorem Cslib.Crypto.MACScheme.eval_eufCmaGame_eq_signingPairOracle (M : MACScheme) (adversary : Forger) (n : ℕ) :
                      (M.eufCmaGame adversary n).eval = (do let sk ← M.keyGen n let out ← (OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (adversary n [])).run [] pure (out.1.1.length == n && !(List.map Prod.fst out.2).contains out.1.1 && M.verify sk out.1.1 out.1.2)).eval

                      eufCmaGame evaluates the same pair-logging execution signingPairOracle as sufCmaGame, checking message freshness !(out.2.map Prod.fst).contains out.1.1 on the projected message log.

                      source
                      theorem Cslib.Crypto.MACScheme.succProbability_eufCmaGame_le_sufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) :
                      Game.succProbability (M.eufCmaGame adversary n).eval ≤ Game.succProbability (M.sufCmaGame adversary n).eval

                      Quantitative EUF-CMA vs. SUF-CMA bound: for every MACScheme, adaptive forger, and security parameter n, the fresh-message EUF-CMA forgery probability is at most the strong fresh-pair SUF-CMA forgery probability.

                      source
                      theorem Cslib.Crypto.MACScheme.SUFCMA.eufCma {M : MACScheme} (h : M.SUFCMA) :
                      M.EUFCMA

                      Strong unforgeability (SUFCMA) implies ordinary fresh-message unforgeability (EUFCMA) for every MACScheme.

                      source
                      theorem Cslib.Crypto.MACScheme.SUFCMA.oneTimeEUFCMA {M : MACScheme} (h : M.SUFCMA) :
                      M.OneTimeEUFCMA

                      Strong unforgeability (SUFCMA) implies one-time unforgeability (OneTimeEUFCMA) for every MACScheme.

                      source
                      theorem Cslib.Crypto.MACScheme.eval_sufCmaGame_eq_eufCmaGame_of_unique_tag (M : MACScheme) (huniq : ∀ (n : ℕ), ∀ sk ∈ (M.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ (tag tag' : List Bool), M.verify sk msg tag = true → tag' ∈ (M.sign sk msg).eval.support → tag' = tag) (adversary : Forger) (n : ℕ) :
                      (M.sufCmaGame adversary n).eval = (M.eufCmaGame adversary n).eval

                      For any MACScheme whose valid tags on n-bit messages under supported secret keys agree with every tag in the support of M.sign, the sufCmaGame and eufCmaGame distributions are identical.

                      source
                      theorem Cslib.Crypto.MACScheme.succProbability_sufCmaGame_eq_eufCmaGame_of_unique_tag (M : MACScheme) (huniq : ∀ (n : ℕ), ∀ sk ∈ (M.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ (tag tag' : List Bool), M.verify sk msg tag = true → tag' ∈ (M.sign sk msg).eval.support → tag' = tag) (adversary : Forger) (n : ℕ) :
                      Game.succProbability (M.sufCmaGame adversary n).eval = Game.succProbability (M.eufCmaGame adversary n).eval

                      For a MACScheme with unique valid tags per (sk, msg), the SUF-CMA and EUF-CMA forgery probabilities are equal for every forger and security parameter n.

                      source
                      theorem Cslib.Crypto.MACScheme.sufCma_iff_eufCma_of_unique_tag (M : MACScheme) (huniq : ∀ (n : ℕ), ∀ sk ∈ (M.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = n → ∀ (tag tag' : List Bool), M.verify sk msg tag = true → tag' ∈ (M.sign sk msg).eval.support → tag' = tag) :
                      M.SUFCMA ↔ M.EUFCMA

                      For a MACScheme with unique valid tags per (sk, msg), strong unforgeability (SUFCMA) is equivalent to ordinary fresh-message unforgeability (EUFCMA).

                      Canonical PRF-based MAC (prfMAC, Boneh–Shoup Section 6.3 & Theorem 6.2) #

                      source
                      noncomputable def Cslib.Crypto.prfMAC (family : List Bool → List Bool → List Bool) (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
                      MACScheme

                      Canonical deterministic MAC constructed from a keyed function family family (Boneh and Shoup, Section 6.3):

                      • keyGen n samples a uniform n-bit key via BitString.sampleList n.
                      • sign sk msg returns prfOracle family sk.length sk msg (which evaluates family sk msg on sk.length-bit messages and rejects malformed queries with []).
                      • verify sk msg tag checks msg.length == sk.length and family sk msg == tag.
                      Instances For
                        source
                        def Cslib.Crypto.macLogHandler (n : ℕ) (request : Unit × List Bool) :
                        StateT (List (List Bool)) (Probability.WordOracleComp Unit) (List Bool)

                        Open stateful handler that forwards each MAC signing request to the external PRF/random-function oracle (truncating the reply to n bits) and records the queried message in the query log.

                        Instances For
                          source
                          def Cslib.Crypto.macToPrfDistinguisher (adversary : Forger) :
                          OracleDistinguisher

                          Oracle reduction turning an adaptive MAC forger adversary into an OracleDistinguisher for the PRF security game Boneh and Shoup, Section 6.3, Theorem 6.2:

                          1. Run adversary n [], answering each tagging query via macLogHandler n and logging all queried messages.
                          2. When adversary outputs ((msg, tag), queried), if msg.length == n and !queried.contains msg, query the external oracle once on msg (reading at most n bits) and check whether the reply equals tag; otherwise return false.
                          Instances For
                            source
                            theorem Cslib.Crypto.isOraclePPT_macToPrfDistinguisher {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) :
                            Probability.IsOraclePPT Turing.MultiTapeTM.encBool (macToPrfDistinguisher adversary)

                            macToPrfDistinguisher preserves strict oracle-PPT admissibility (IsOraclePPT).

                            source
                            theorem Cslib.Crypto.eval_prfRealGame_macToPrfDistinguisher {family : List Bool → List Bool → List Bool} (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (adversary : Forger) (n : ℕ) :
                            (prfRealGame family (macToPrfDistinguisher adversary) n).eval = ((prfMAC family hpoly).eufCmaGame adversary n).eval

                            Running macToPrfDistinguisher adversary in prfRealGame family produces the exact same Boolean distribution as the EUF-CMA experiment for prfMAC family.

                            source
                            theorem Cslib.Crypto.succProbability_prfIdealGame_macToPrfDistinguisher_le (adversary : Forger) (n : ℕ) :
                            Game.succProbability (prfIdealGame (macToPrfDistinguisher adversary) n).eval ≤ 1 / 2 ^ n

                            In the ideal random-function game, macToPrfDistinguisher adversary succeeds with probability at most 1 / 2 ^ n: any unqueried n-bit forgery message misses the lazy random-oracle cache and draws a fresh uniform n-bit tag, matching the forger's candidate tag with probability at most 1 / 2 ^ n.

                            source
                            theorem Cslib.Crypto.eval_sufCmaGame_prfMAC {family : List Bool → List Bool → List Bool} (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (adversary : Forger) (n : ℕ) :
                            ((prfMAC family hpoly).sufCmaGame adversary n).eval = ((prfMAC family hpoly).eufCmaGame adversary n).eval

                            Because prfMAC is deterministic with a unique valid tag per (sk, msg), its strong fresh-pair sufCmaGame distribution is identical to its fresh-message eufCmaGame distribution.

                            source
                            theorem Cslib.Crypto.sufCma_prfMAC_iff_eufCma {family : List Bool → List Bool → List Bool} (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) :
                            (prfMAC family hpoly).SUFCMA ↔ (prfMAC family hpoly).EUFCMA

                            For prfMAC, strong unforgeability (SUFCMA) and fresh-message unforgeability (EUFCMA) coincide.

                            source
                            theorem Cslib.Crypto.eval_prfRealGame_macToPrfDistinguisher_eq_sufCmaGame {family : List Bool → List Bool → List Bool} (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (adversary : Forger) (n : ℕ) :
                            (prfRealGame family (macToPrfDistinguisher adversary) n).eval = ((prfMAC family hpoly).sufCmaGame adversary n).eval

                            Running macToPrfDistinguisher adversary in prfRealGame family produces the exact same Boolean distribution as the strong SUF-CMA experiment for prfMAC family.

                            source
                            theorem Cslib.Crypto.succProbability_eufCmaGame_prfMAC_le {family : List Bool → List Bool → List Bool} (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (adversary : Forger) (n : ℕ) :
                            Game.succProbability ((prfMAC family hpoly).eufCmaGame adversary n).eval ≤ Game.advantage (prfRealGame family (macToPrfDistinguisher adversary) n).eval (prfIdealGame (macToPrfDistinguisher adversary) n).eval + 1 / 2 ^ n

                            Quantitative PRF-to-MAC forgery bound Boneh and Shoup, Theorem 6.2: for every adaptive MAC forger adversary and every security parameter n, the EUF-CMA forgery probability against prfMAC family is at most the PRF distinguishing advantage of macToPrfDistinguisher adversary plus 1 / 2 ^ n.

                            source
                            theorem Cslib.Crypto.succProbability_sufCmaGame_prfMAC_le {family : List Bool → List Bool → List Bool} (hpoly : Turing.MultiTapeTM.ComputableInPolyTime (fun (pair : List Bool × List Bool) => family pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (hlen : ∀ (key query : List Bool), query.length = key.length → (family key query).length = key.length) (adversary : Forger) (n : ℕ) :
                            Game.succProbability ((prfMAC family hpoly).sufCmaGame adversary n).eval ≤ Game.advantage (prfRealGame family (macToPrfDistinguisher adversary) n).eval (prfIdealGame (macToPrfDistinguisher adversary) n).eval + 1 / 2 ^ n

                            Quantitative PRF-to-SUF-CMA forgery bound Boneh and Shoup, Theorem 6.2: for every adaptive MAC forger adversary and every security parameter n, the strong SUF-CMA forgery probability against prfMAC family is at most the PRF distinguishing advantage of macToPrfDistinguisher adversary plus 1 / 2 ^ n.

                            source
                            theorem Cslib.Crypto.PseudorandomFunction.eufCma_prfMAC {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) :
                            (prfMAC family ⋯).EUFCMA

                            PRF-to-MAC security theorem Boneh and Shoup, Theorem 6.2: every uniform PseudorandomFunction yields an EUFCMA-secure MACScheme.

                            source
                            theorem Cslib.Crypto.PseudorandomFunction.sufCma_prfMAC {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) :
                            (prfMAC family ⋯).SUFCMA

                            PRF-to-SUF-CMA security theorem Boneh and Shoup, Theorem 6.2: every uniform PseudorandomFunction yields a strongly unforgeable (SUFCMA) MACScheme.

                            source
                            theorem Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_prfMAC {family : List Bool → List Bool → List Bool} (hprf : PseudorandomFunction family) :
                            (prfMAC family ⋯).OneTimeEUFCMA

                            Every uniform PseudorandomFunction also yields a OneTimeEUFCMA-secure MACScheme.