Uniform message authentication codes and PRF-based MACs

A uniform symmetric message authentication code (MACScheme) consists of a polynomial-time message-length schedule msgLen : ℕ → ℕ (defaulting to id), 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 a msgLen 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 msgLen 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 also provide schedule reindexing (MACScheme.reindex, MACScheme.reindexForger, SUFCMA.reindex, EUFCMA.reindex, OneTimeEUFCMA.reindex), which adapts any MACScheme along a strictly monotone polynomial-time parameter schedule ℓ : ℕ → ℕ so that at security parameter n it authenticates M.msgLen (ℓ n)-bit messages. 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

• Cslib.Crypto.MACScheme: uniform symmetric message authentication code on msgLen n-bit messages (defaulting to n-bit messages).
• Cslib.Crypto.MACScheme.signingPairOracle, sufCmaGame, SUFCMA: pair-logging tagging oracle and strong (fresh-pair) adaptive SUF-CMA experiment and security predicate (Boneh and Shoup, Attack Game 6.1 / Definition 6.2).
• Cslib.Crypto.MACScheme.signingOracle, eufCmaGame, EUFCMA: fresh-message adaptive EUF-CMA experiment and security predicate.
• Cslib.Crypto.MACScheme.oneTimeSigningOracle, eufOneTimeGame, OneTimeEUFCMA: one-time fresh-message adaptive EUF-CMA experiment and security predicate.
• Cslib.Crypto.MACScheme.reindex, Cslib.Crypto.MACScheme.reindexForger: schedule reindexing of a MACScheme and its adaptive forger reduction (via GeneratorReindex.parameter).
• Cslib.Crypto.prfMAC: canonical deterministic MAC constructed from a keyed function family (Boneh and Shoup, Section 6.3).
• Cslib.Crypto.macLogHandler, Cslib.Crypto.macToPrfDistinguisher: oracle logging handler and reduction turning a MAC forger into a PRF distinguisher.
• Cslib.Crypto.NonceMACForger, Cslib.Crypto.NonceMACScheme: uniform nonce-based message authentication code (sign : Key → Msg → Nonce → ProbComp Tag) and adaptive forger (Boneh and Shoup, Section 7.5, Attack Game 7.4).
• Cslib.Crypto.NonceMACScheme.signingPairOracle, sufCmaGame, eufCmaGame, SUFCMA, EUFCMA: nonce-respecting adaptive chosen-message security experiments and predicates requiring distinct queried nonces ((tr.map (fun e => e.1.2)).Nodup).

Main results

• Cslib.Crypto.MACScheme.isPPTOn_sufCmaGame, isPPT_sufCmaGame, isPPTOn_eufCmaGame, isPPT_eufCmaGame: strict PPT certificates for the MAC SUF-CMA and EUF-CMA experiments.
• Cslib.Crypto.MACScheme.eval_run_signingOracle_eq_map_fst_signingPairOracle, eval_eufCmaGame_eq_signingPairOracle, succProbability_eufCmaGame_le_sufCmaGame, SUFCMA.eufCma, SUFCMA.oneTimeEUFCMA: shared pair-history representation and quantitative / asymptotic implication from strong to ordinary unforgeability.
• Cslib.Crypto.MACScheme.eval_sufCmaGame_eq_eufCmaGame_of_unique_tag, sufCma_iff_eufCma_of_unique_tag: equivalence of SUF-CMA and EUF-CMA for MACs with a unique valid tag per message.
• Cslib.Crypto.MACScheme.isPPTOn_eufOneTimeGame, isPPT_eufOneTimeGame: strict PPT certificates for the one-time MAC EUF-CMA experiment.
• Cslib.Crypto.MACScheme.EUFCMA.oneTimeEUFCMA: full EUF-CMA security implies one-time EUF-CMA security.
• Cslib.Crypto.MACScheme.isOraclePPT_reindexForger, Cslib.Crypto.MACScheme.sufCmaGame_reindex, Cslib.Crypto.MACScheme.eufCmaGame_reindex, Cslib.Crypto.MACScheme.eufOneTimeGame_reindex, Cslib.Crypto.MACScheme.SUFCMA.reindex, Cslib.Crypto.MACScheme.EUFCMA.reindex, Cslib.Crypto.MACScheme.OneTimeEUFCMA.reindex: schedule reindexing preserves SUFCMA, EUFCMA, and OneTimeEUFCMA along any strictly monotone polynomial-time schedule.
• Cslib.Crypto.eval_sufCmaGame_prfMAC, Cslib.Crypto.sufCma_prfMAC_iff_eufCma, Cslib.Crypto.isOraclePPT_macToPrfDistinguisher, Cslib.Crypto.eval_prfRealGame_macToPrfDistinguisher, Cslib.Crypto.eval_prfRealGame_macToPrfDistinguisher_eq_sufCmaGame, Cslib.Crypto.succProbability_prfIdealGame_macToPrfDistinguisher_le, Cslib.Crypto.succProbability_eufCmaGame_prfMAC_le, Cslib.Crypto.succProbability_sufCmaGame_prfMAC_le: quantitative PRF-to-MAC forgery reduction (Boneh and Shoup, Theorem 6.2).
• Cslib.Crypto.PseudorandomFunction.sufCma_prfMAC, Cslib.Crypto.PseudorandomFunction.eufCma_prfMAC, Cslib.Crypto.PseudorandomFunction.oneTimeEUFCMA_prfMAC: any secure uniform PseudorandomFunction yields a SUFCMA-, EUFCMA-, and OneTimeEUFCMA-secure MACScheme.
• Cslib.Crypto.NonceMACScheme.isPPTOn_run_signingPairOracle, Cslib.Crypto.NonceMACScheme.isPPTOn_sufCmaGame, isPPT_sufCmaGame, isPPTOn_eufCmaGame, isPPT_eufCmaGame, succProbability_eufCmaGame_le_sufCmaGame, SUFCMA.eufCma, eval_sufCmaGame_eq_freshPair_of_unique_tag: strict PPT certificates, quantitative / asymptotic implication from SUFCMA to EUFCMA, and unique-tag pair-freshness characterization for nonce-based MACs.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Chapter 6, Sections 6.1–6.3 (Definitions 6.1–6.2 and Theorem 6.2) and Chapter 7, Section 7.5 (Attack Game 7.4).
• O. Goldreich, S. Goldwasser, S. Micali, How to Construct Random Functions.

structure Cslib.Crypto.MACScheme : Type

A uniform symmetric message authentication code (MAC) on msgLen n-bit messages at security parameter n (defaulting to msgLen = id, i.e., n-bit messages), with plain polynomial-time message-length schedule, strict polynomial-time key generation and tag generation, deterministic polynomial-time verification, and perfect completeness on supported keys, msgLen n-bit messages, and tags Boneh and Shoup, Definition 6.1.

• msgLen : ℕ → ℕ

  Message length authenticated at unary security parameter n (defaults to n).

• msgLen_polyTime : Turing.MultiTapeTM.ComputableInPolyTime self.msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  The message-length schedule is computable in plain polynomial time in unary.

• keyGen : ℕ → ProbComp (List Bool)

  Sample a secret MAC key sk at unary security parameter n.

• sign : List Bool → List Bool → ProbComp (List Bool)

  Compute a MAC tag on message msg using the secret key sk.

• verify : List Bool → List Bool → List Bool → Bool

  Deterministically verify a candidate tag on msg under secret key sk.

• keyGen_ppt : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits self.keyGen

  Key generation is uniformly strict PPT in the unary security parameter.

• sign_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits fun (p : List Bool × List Bool) => self.sign p.1 p.2

  Tag generation is uniformly strict PPT in the encoded secret key and message.

• verify_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List Bool) => self.verify p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBool

  Verification is computable in plain polynomial time on (sk, msg, tag).

• verify_sign (n : ℕ) (sk : List Bool) : sk ∈ (self.keyGen n).eval.support → ∀ (msg : List Bool), msg.length = self.msgLen n → ∀ tag ∈ (self.sign sk msg).eval.support, self.verify sk msg tag = true

  Every tag produced by sign on a msgLen n-bit message under a supported secret key at security parameter n is accepted by verify.

theorem Cslib.Crypto.MACScheme.computableInPolyTime_msgLen_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => M.msgLen (n a)) encIn Turing.MultiTapeTM.encUnary

Composing M.msgLen with a plain polynomial-time unary parameter function is plain polynomial-time.

theorem Cslib.Crypto.MACScheme.isPPTOn_keyGen_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encBits fun (a : γ) => M.keyGen (n a)

Composing M.keyGen with a plain polynomial-time unary parameter function is strict PPT.

theorem Cslib.Crypto.MACScheme.isPPTOn_sign_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ List Bool} {sk msg : γ → List Bool} (hsk : Turing.MultiTapeTM.ComputableInPolyTime sk encIn Turing.MultiTapeTM.encBits) (hmsg : Turing.MultiTapeTM.ComputableInPolyTime msg encIn Turing.MultiTapeTM.encBits) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encBits fun (a : γ) => M.sign (sk a) (msg a)

Composing M.sign with plain polynomial-time key and message selectors is strict PPT.

theorem Cslib.Crypto.MACScheme.computableInPolyTime_verify_comp (M : MACScheme) {γ : Type} {encIn : γ ↪ List Bool} {sk msg tag : γ → List Bool} (hsk : Turing.MultiTapeTM.ComputableInPolyTime sk encIn Turing.MultiTapeTM.encBits) (hmsg : Turing.MultiTapeTM.ComputableInPolyTime msg encIn Turing.MultiTapeTM.encBits) (htag : Turing.MultiTapeTM.ComputableInPolyTime tag encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => M.verify (sk a) (msg a) (tag a)) encIn Turing.MultiTapeTM.encBool

Composing M.verify with plain polynomial-time key, message, and tag selectors is plain polynomial-time.

Full adaptive chosen-message security (EUFCMA)

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.

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 a M.msgLen 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.

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.

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.

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.

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.

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)

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.

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 a M.msgLen n-bit message distinct from the queried message (if any).

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.

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.

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.

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

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

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.

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.

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)

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

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 a M.msgLen n-bit message msg such that (msg, tag) was never returned by the tagging oracle (!out.2.contains out.1).

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.

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.

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.

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

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.

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.

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.

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 == M.msgLen 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.

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.

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.

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

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

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 = M.msgLen 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 M.msgLen n-bit messages under supported secret keys agree with every tag in the support of M.sign, the sufCmaGame and eufCmaGame distributions are identical.

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 = M.msgLen 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.

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 = M.msgLen 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).

Schedule reindexing of a MACScheme (reindex, reindexForger)

noncomputable def Cslib.Crypto.MACScheme.reindex (M : MACScheme) (ℓ : ℕ → ℕ) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : MACScheme

Reindex a MACScheme along a polynomial-time parameter schedule ℓ : ℕ → ℕ: at security parameter n, M.reindex ℓ hℓ samples keys via M.keyGen (ℓ n) and authenticates messages of length M.msgLen (ℓ n).

def Cslib.Crypto.MACScheme.reindexForger (ℓ : ℕ → ℕ) (adversary : Forger) : Forger

Wrap a forger adversary against M.reindex ℓ hℓ into a forger against M: given unary parameter m and auxiliary input aux, recover n := GeneratorReindex.parameter ℓ m; if ℓ n == m, run adversary n aux, and otherwise return ([], []) without querying the oracle.

@[simp]

theorem Cslib.Crypto.MACScheme.reindexForger_apply_of_strictMono {ℓ : ℕ → ℕ} (hmono : StrictMono ℓ) (adversary : Forger) (n : ℕ) (aux : List Bool) : reindexForger ℓ adversary (ℓ n) aux = adversary n aux

At any parameter m = ℓ n of a strictly monotone schedule ℓ, reindexForger ℓ adversary executes adversary n.

theorem Cslib.Crypto.MACScheme.isOraclePPT_reindexForger {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (reindexForger ℓ adversary)

reindexForger ℓ adversary preserves strict oracle-PPT admissibility (IsOraclePPT).

@[simp]

theorem Cslib.Crypto.MACScheme.sufCmaGame_reindex (M : MACScheme) {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmono : StrictMono ℓ) (adversary : Forger) (n : ℕ) : (M.reindex ℓ hℓ).sufCmaGame adversary n = M.sufCmaGame (reindexForger ℓ adversary) (ℓ n)

For a strictly monotone schedule ℓ, (M.reindex ℓ hℓ).sufCmaGame adversary n is identical to M.sufCmaGame (reindexForger ℓ adversary) (ℓ n).

@[simp]

theorem Cslib.Crypto.MACScheme.eufCmaGame_reindex (M : MACScheme) {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmono : StrictMono ℓ) (adversary : Forger) (n : ℕ) : (M.reindex ℓ hℓ).eufCmaGame adversary n = M.eufCmaGame (reindexForger ℓ adversary) (ℓ n)

For a strictly monotone schedule ℓ, (M.reindex ℓ hℓ).eufCmaGame adversary n is identical to M.eufCmaGame (reindexForger ℓ adversary) (ℓ n).

@[simp]

theorem Cslib.Crypto.MACScheme.eufOneTimeGame_reindex (M : MACScheme) {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmono : StrictMono ℓ) (adversary : Forger) (n : ℕ) : (M.reindex ℓ hℓ).eufOneTimeGame adversary n = M.eufOneTimeGame (reindexForger ℓ adversary) (ℓ n)

For a strictly monotone schedule ℓ, (M.reindex ℓ hℓ).eufOneTimeGame adversary n is identical to M.eufOneTimeGame (reindexForger ℓ adversary) (ℓ n).

theorem Cslib.Crypto.MACScheme.SUFCMA.reindex {M : MACScheme} (h : M.SUFCMA) {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmono : StrictMono ℓ) : (M.reindex ℓ hℓ).SUFCMA

Strong unforgeability (SUFCMA) is preserved under reindexing along any strictly monotone plain polynomial-time schedule ℓ.

theorem Cslib.Crypto.MACScheme.EUFCMA.reindex {M : MACScheme} (h : M.EUFCMA) {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmono : StrictMono ℓ) : (M.reindex ℓ hℓ).EUFCMA

Ordinary fresh-message unforgeability (EUFCMA) is preserved under reindexing along any strictly monotone plain polynomial-time schedule ℓ.

theorem Cslib.Crypto.MACScheme.OneTimeEUFCMA.reindex {M : MACScheme} (h : M.OneTimeEUFCMA) {ℓ : ℕ → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hmono : StrictMono ℓ) : (M.reindex ℓ hℓ).OneTimeEUFCMA

One-time unforgeability (OneTimeEUFCMA) is preserved under reindexing along any strictly monotone plain polynomial-time schedule ℓ.

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

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.

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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Nonce-based message authentication codes (NonceMACScheme, Boneh–Shoup Section 7.5)

@[reducible, inline]

abbrev Cslib.Crypto.NonceMACForger : Type

An adaptive nonce-based MAC forger receives a unary security parameter and an auxiliary word, queries a nonce-respecting tagging oracle on encoded (message, nonce) pairs (encPair encBits encBits (msg, nonce)), and outputs a candidate ((message, nonce), tag) triple (Boneh and Shoup, Section 7.5, Attack Game 7.4).

structure Cslib.Crypto.NonceMACScheme : Type

A uniform symmetric nonce-based message authentication code (NonceMACScheme) on msgLen n-bit messages and nonceLen n-bit nonces at security parameter n (both defaulting to n), with plain polynomial-time length schedules, strict polynomial-time key generation and tag generation, deterministic polynomial-time verification, and perfect completeness on supported keys, msgLen n-bit messages, nonceLen n-bit nonces, and tags (Boneh and Shoup, Section 7.5, Attack Game 7.4).

• msgLen : ℕ → ℕ

  Message length authenticated at unary security parameter n (defaults to n).

• msgLen_polyTime : Turing.MultiTapeTM.ComputableInPolyTime self.msgLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  The message-length schedule is computable in plain polynomial time in unary.

• nonceLen : ℕ → ℕ

  Nonce length required at unary security parameter n (defaults to n).

• nonceLen_polyTime : Turing.MultiTapeTM.ComputableInPolyTime self.nonceLen Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  The nonce-length schedule is computable in plain polynomial time in unary.

• keyGen : ℕ → ProbComp (List Bool)

  Sample a secret MAC key sk at unary security parameter n.

• sign : List Bool → List Bool → List Bool → ProbComp (List Bool)

  Compute a MAC tag on message msg and nonce nonce using the secret key sk.

• verify : List Bool → List Bool → List Bool → List Bool → Bool

  Deterministically verify a candidate tag on (msg, nonce) under secret key sk.

• keyGen_ppt : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits self.keyGen

  Key generation is uniformly strict PPT in the unary security parameter.

• sign_ppt : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : List Bool × List Bool × List Bool) => self.sign p.1 p.2.1 p.2.2

  Tag generation is uniformly strict PPT in the encoded (sk, msg, nonce).

• verify_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × List Bool × List Bool × List Bool) => self.verify p.1 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBool

  Verification is computable in plain polynomial time on (sk, msg, nonce, tag).

• verify_sign (n : ℕ) (sk : List Bool) : sk ∈ (self.keyGen n).eval.support → ∀ (msg : List Bool), msg.length = self.msgLen n → ∀ (nonce : List Bool), nonce.length = self.nonceLen n → ∀ tag ∈ (self.sign sk msg nonce).eval.support, self.verify sk msg nonce tag = true

  Every tag produced by sign on a msgLen n-bit message and nonceLen n-bit nonce under a supported secret key at security parameter n is accepted by verify.

theorem Cslib.Crypto.length_unframe_add_dropFrame_le (v : List Bool) : 2 * (Turing.MultiTapeTM.unframe v).length + (Turing.MultiTapeTM.dropFrame v).length ≤ v.length

The unframed prefix and remaining suffix of any bit list satisfy 2 * (unframe v).length + (dropFrame v).length ≤ v.length.

theorem Cslib.Crypto.NonceMACScheme.computableInPolyTime_msgLen_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => M.msgLen (n a)) encIn Turing.MultiTapeTM.encUnary

Composing M.msgLen with a plain polynomial-time unary parameter function is plain polynomial-time.

theorem Cslib.Crypto.NonceMACScheme.computableInPolyTime_nonceLen_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => M.nonceLen (n a)) encIn Turing.MultiTapeTM.encUnary

Composing M.nonceLen with a plain polynomial-time unary parameter function is plain polynomial-time.

theorem Cslib.Crypto.NonceMACScheme.isPPTOn_keyGen_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} {n : γ → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encBits fun (a : γ) => M.keyGen (n a)

Composing M.keyGen with a plain polynomial-time unary parameter function is strict PPT.

theorem Cslib.Crypto.NonceMACScheme.isPPTOn_sign_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} {sk msg nonce : γ → List Bool} (hsk : Turing.MultiTapeTM.ComputableInPolyTime sk encIn Turing.MultiTapeTM.encBits) (hmsg : Turing.MultiTapeTM.ComputableInPolyTime msg encIn Turing.MultiTapeTM.encBits) (hnonce : Turing.MultiTapeTM.ComputableInPolyTime nonce encIn Turing.MultiTapeTM.encBits) : Probability.IsPPTOn encIn Turing.MultiTapeTM.encBits fun (a : γ) => M.sign (sk a) (msg a) (nonce a)

Composing M.sign with plain polynomial-time key, message, and nonce selectors is strict PPT.

theorem Cslib.Crypto.NonceMACScheme.computableInPolyTime_verify_comp (M : NonceMACScheme) {γ : Type} {encIn : γ ↪ List Bool} {sk msg nonce tag : γ → List Bool} (hsk : Turing.MultiTapeTM.ComputableInPolyTime sk encIn Turing.MultiTapeTM.encBits) (hmsg : Turing.MultiTapeTM.ComputableInPolyTime msg encIn Turing.MultiTapeTM.encBits) (hnonce : Turing.MultiTapeTM.ComputableInPolyTime nonce encIn Turing.MultiTapeTM.encBits) (htag : Turing.MultiTapeTM.ComputableInPolyTime tag encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => M.verify (sk a) (msg a) (nonce a) (tag a)) encIn Turing.MultiTapeTM.encBool

Composing M.verify with plain polynomial-time key, message, nonce, and tag selectors is plain polynomial-time.

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

Stateful nonce-based MAC tagging oracle that decodes (msg, nonce) from the framed query word request.2, tags (msg, nonce) under sk, and prepends the returned ((msg, nonce), tag) triple to the transcript (Boneh and Shoup, Section 7.5, Attack Game 7.4).

noncomputable def Cslib.Crypto.NonceMACScheme.sufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (n : ℕ) : ProbComp Bool

The strong nonce-based MAC SUF-CMA experiment (Boneh and Shoup, Section 7.5, Attack Game 7.4): sample sk ← M.keyGen n, run the adaptive forger on (n, []) with oracle access to M.signingPairOracle sk, and accept when:

1. the candidate message has length M.msgLen n and the candidate nonce has length M.nonceLen n,
2. all nonces queried during the signing phase are pairwise distinct (decide (out.2.map (fun e => e.1.2)).Nodup),
3. the candidate ((msg, nonce), tag) triple was never returned by the tagging oracle (!out.2.contains out.1), and
4. M.verify sk msg nonce tag = true.

noncomputable def Cslib.Crypto.NonceMACScheme.eufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (n : ℕ) : ProbComp Bool

The fresh-message nonce-based MAC EUF-CMA experiment: identical to sufCmaGame except that the candidate message out.1.1.1 must never have been queried during the signing phase (!(out.2.map (fun e => e.1.1)).contains out.1.1.1).

theorem Cslib.Crypto.NonceMACScheme.isPPTOn_run_signingPairOracle (M : NonceMACScheme) {adversary : NonceMACForger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits 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.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits 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 nonce-MAC forger against signingPairOracle is uniformly strict PPT in the unary security parameter and secret key.

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

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

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

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

theorem Cslib.Crypto.NonceMACScheme.isPPTOn_eufCmaGame (M : NonceMACScheme) {adversary : NonceMACForger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (M.eufCmaGame adversary)

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

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

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

def Cslib.Crypto.NonceMACScheme.SUFCMA (M : NonceMACScheme) : Prop

Strong existential unforgeability under nonce-respecting adaptive chosen-message attack (SUFCMA) for a NonceMACScheme against uniform strict oracle-PPT adversaries (Boneh and Shoup, Section 7.5, Attack Game 7.4).

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

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

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

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

def Cslib.Crypto.NonceMACScheme.EUFCMA (M : NonceMACScheme) : Prop

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

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

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

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

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

theorem Cslib.Crypto.NonceMACScheme.succProbability_eufCmaGame_le_sufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) (n : ℕ) : Game.succProbability (M.eufCmaGame adversary n).eval ≤ Game.succProbability (M.sufCmaGame adversary n).eval

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

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

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

theorem Cslib.Crypto.NonceMACScheme.eval_sufCmaGame_eq_freshPair_of_unique_tag (M : NonceMACScheme) (huniq : ∀ (n : ℕ), ∀ sk ∈ (M.keyGen n).eval.support, ∀ (msg : List Bool), msg.length = M.msgLen n → ∀ (nonce : List Bool), nonce.length = M.nonceLen n → ∀ (tag tag' : List Bool), M.verify sk msg nonce tag = true → tag' ∈ (M.sign sk msg nonce).eval.support → tag' = tag) (adversary : NonceMACForger) (n : ℕ) : (M.sufCmaGame 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.1.length == M.msgLen n && out.1.1.2.length == M.nonceLen n && decide (List.map (fun (e : (List Bool × List Bool) × List Bool) => e.1.2) out.2).Nodup && !(List.map Prod.fst out.2).contains out.1.1 && M.verify sk out.1.1.1 out.1.1.2 out.1.2)).eval

For any NonceMACScheme whose valid tags on M.msgLen n-bit messages and M.nonceLen n-bit nonces under supported secret keys agree with every tag in the support of M.sign, strong triple-freshness (!out.2.contains out.1) in sufCmaGame is identical to (msg, nonce)-pair freshness (!(out.2.map Prod.fst).contains out.1.1).