Uniform digital signature schemes and existential unforgeability

A uniform digital signature scheme (SignatureScheme) consists of a strict probabilistic polynomial-time key generator keyGen, a strict probabilistic polynomial-time signing algorithm sign, and a deterministic polynomial-time verification algorithm verify that accepts every signature produced by sign on an n-bit message under a key pair sampled at security parameter n. The message space at parameter n is exactly the n-bit words; this module does not claim security for arbitrary polynomial-length message families.

We formalize two adaptive chosen-message security notions against uniform strict oracle-PPT forgers (IsOraclePPT):

• Existential unforgeability under adaptive chosen-message attack (eufCmaGame, EUFCMA): the forger receives the unary security parameter n and public verification key pk, has adaptive oracle access to signingOracle sk on arbitrary messages, and wins by outputting a valid (msg, sig) pair with msg.length = n such that msg was never queried to the signing oracle.
• Existential unforgeability under one-time adaptive chosen-message attack (eufOneTimeGame, OneTimeEUFCMA): the signing oracle oneTimeSigningOracle sk answers at most the first signing query and returns the empty word on any subsequent query. Every EUFCMA-secure scheme is a fortiori OneTimeEUFCMA-secure (SignatureScheme.EUFCMA.oneTimeEUFCMA).

Main definitions

• Cslib.Crypto.Forger: adaptive oracle adversary outputting a (message, signature) pair.
• Cslib.Crypto.SignatureScheme: uniform digital signature scheme on n-bit messages.
• Cslib.Crypto.SignatureScheme.signingOracle, eufCmaGame, EUFCMA: full adaptive EUF-CMA experiment and security predicate.
• Cslib.Crypto.SignatureScheme.oneTimeSigningOracle, eufOneTimeGame, OneTimeEUFCMA: one-time adaptive EUF-CMA experiment and security predicate.

Main results

• Cslib.Crypto.SignatureScheme.isPPTOn_eufCmaGame, isPPT_eufCmaGame: strict PPT certificates for the full EUF-CMA experiment.
• Cslib.Crypto.SignatureScheme.isPPTOn_eufOneTimeGame, isPPT_eufOneTimeGame: strict PPT certificates for the one-time EUF-CMA experiment.
• Cslib.Crypto.SignatureScheme.EUFCMA.oneTimeEUFCMA: full EUF-CMA security implies one-time EUF-CMA security.

References

• S. Goldwasser, S. Micali, R. L. Rivest, A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks
• L. Lamport, Constructing Digital Signatures from a One-Way Function
• J. Rompel, One-Way Functions are Necessary and Sufficient for Secure Signatures

@[reducible, inline]

abbrev Cslib.Crypto.Forger : Type

An adaptive forger receives a unary security parameter and a public verification key, queries a signing oracle on chosen messages, and outputs a candidate (message, signature) pair.

structure Cslib.Crypto.SignatureScheme : Type

A uniform digital signature scheme on n-bit messages at security parameter n, with strict polynomial-time key generation and signing, deterministic polynomial-time verification, and perfect completeness on supported key pairs, n-bit messages, and signatures.

• keyGen : ℕ → ProbComp (List Bool × List Bool)

  Sample a public verification key and secret signing key (pk, sk) at unary parameter n.

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

  Sign a message msg using the secret signing key sk.

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

  Deterministically verify a candidate signature sig on msg under public key pk.

• keyGen_ppt : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits 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

  Signing 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 (pk, msg, sig).

• verify_sign (n : ℕ) (keys : List Bool × List Bool) : keys ∈ (self.keyGen n).eval.support → ∀ (msg : List Bool), msg.length = n → ∀ sig ∈ (self.sign keys.2 msg).eval.support, self.verify keys.1 msg sig = true

  Every signature produced by sign on an n-bit message under a supported key pair at security parameter n is accepted by verify.

theorem Cslib.Crypto.SignatureScheme.verify_polyTime_tidy (h : SignatureScheme) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × List Bool × List Bool) => h.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

The equivalent tidy contract used internally by compositional proofs.

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

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

theorem Cslib.Crypto.SignatureScheme.computableTidilyInPolyTime_verify_comp (S : SignatureScheme) {γ : Type} {encIn : γ ↪ List Bool} {pk msg sig : γ → List Bool} (hpk : Turing.MultiTapeTM.ComputableTidilyInPolyTime pk encIn Turing.MultiTapeTM.encBits) (hmsg : Turing.MultiTapeTM.ComputableTidilyInPolyTime msg encIn Turing.MultiTapeTM.encBits) (hsig : Turing.MultiTapeTM.ComputableTidilyInPolyTime sig encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : γ) => S.verify (pk a) (msg a) (sig a)) encIn Turing.MultiTapeTM.encBool

Full adaptive chosen-message security (EUFCMA)

def Cslib.Crypto.SignatureScheme.signingOracle (S : SignatureScheme) (sk : List Bool) (request : Unit × List Bool) : StateT (List (List Bool)) ProbComp (List Bool)

Stateful signing oracle that signs the requested message under sk and prepends the message to the list of queried messages.

def Cslib.Crypto.SignatureScheme.eufCmaGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) : ProbComp Bool

The EUF-CMA experiment: sample (pk, sk) ← S.keyGen n, run the adaptive forger on (n, pk) with oracle access to S.signingOracle sk, and accept when the forger outputs a valid signature on an n-bit message that was never queried to the signing oracle.

theorem Cslib.Crypto.SignatureScheme.isPPTOn_eufCmaGame (S : SignatureScheme) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (S.eufCmaGame adversary)

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

theorem Cslib.Crypto.SignatureScheme.isPPT_eufCmaGame (S : SignatureScheme) {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) => S.eufCmaGame adversary n

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

def Cslib.Crypto.SignatureScheme.EUFCMA (S : SignatureScheme) : Prop

Existential unforgeability under adaptive chosen-message attack (EUF-CMA) against uniform strict oracle-PPT adversaries.

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

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

theorem Cslib.Crypto.SignatureScheme.EUFCMA.of_negligible {S : SignatureScheme} (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 (S.eufCmaGame adversary n).eval) : S.EUFCMA

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

One-time adaptive chosen-message security (OneTimeEUFCMA)

def Cslib.Crypto.SignatureScheme.oneTimeSigningOracle (S : SignatureScheme) (sk : List Bool) (request : Unit × List Bool) : StateT (List (List Bool)) ProbComp (List Bool)

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

def Cslib.Crypto.SignatureScheme.eufOneTimeGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) : ProbComp Bool

The one-time EUF-CMA experiment: sample (pk, sk) ← S.keyGen n, run the adaptive forger on (n, pk) with oracle access to S.oneTimeSigningOracle sk (which answers at most one signing query), and accept when the forger outputs a valid signature on an n-bit message distinct from the queried message (if any).

theorem Cslib.Crypto.SignatureScheme.isPPTOn_run_oneTimeSigningOracle (S : SignatureScheme) {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.encPair Turing.MultiTapeTM.encBits 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 × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (S.oneTimeSigningOracle caller.2.2)) (adversary caller.1 caller.2.1)).run []

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

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

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

theorem Cslib.Crypto.SignatureScheme.isPPT_eufOneTimeGame (S : SignatureScheme) {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) => S.eufOneTimeGame adversary n

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

def Cslib.Crypto.SignatureScheme.OneTimeEUFCMA (S : SignatureScheme) : Prop

Existential unforgeability under one-time adaptive chosen-message attack against uniform strict oracle-PPT adversaries.

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

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

theorem Cslib.Crypto.SignatureScheme.OneTimeEUFCMA.of_negligible {S : SignatureScheme} (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 (S.eufOneTimeGame adversary n).eval) : S.OneTimeEUFCMA

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

theorem Cslib.Crypto.SignatureScheme.length_le_one_of_mem_support_run_oneTimeSigningOracle (S : SignatureScheme) {α : Type} (sk : List Bool) (prog : Probability.WordOracleComp Unit α) {result : α} {queried : List (List Bool)} (h : (result, queried) ∈ ((OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifOracle k)) fun (q : Unit × List Bool) (s : List (List Bool)) => (S.oneTimeSigningOracle sk q s).eval) prog).run []).support) : queried.length ≤ 1

Starting from the empty query log, oneTimeSigningOracle records at most one queried message.

theorem Cslib.Crypto.SignatureScheme.run_oneTimeSigningOracle_apply_eq_of_agree (S : SignatureScheme) {α : Type} (sk₁ sk₂ : List Bool) {agree : List Bool → Prop} (hagree : ∀ (req : List Bool), agree req → S.sign sk₁ req = S.sign sk₂ req) (prog : Probability.WordOracleComp Unit α) (s : List (List Bool)) (a : α) (queried' : List (List Bool)) (hq' : ∀ r ∈ queried', agree r) : ((OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifOracle k)) fun (q : Unit × List Bool) (s : List (List Bool)) => (S.oneTimeSigningOracle sk₁ q s).eval) prog).run s) (a, queried') = ((OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifOracle k)) fun (q : Unit × List Bool) (s : List (List Bool)) => (S.oneTimeSigningOracle sk₂ q s).eval) prog).run s) (a, queried')

If S.sign sk₁ and S.sign sk₂ agree on all requests satisfying agree, then running any adaptive program against oneTimeSigningOracle under sk₁ and sk₂ assigns the same probability to every outcome (a, queried') whose recorded query log satisfies agree.

Reduction from one-time EUF-CMA to full EUF-CMA

def Cslib.Crypto.SignatureScheme.oneTimeFilterHandler (bound : ℕ → ℕ → ℕ) (caller : ℕ × List Bool) (request : Unit × List Bool) : StateT Bool (Probability.WordOracleComp Unit) (List Bool)

Open stateful handler that forwards at most the first signing request to the external signing oracle (truncating the reply to bound n msg.length) and answers subsequent requests with [].

def Cslib.Crypto.SignatureScheme.limitToOneQuery (bound : ℕ → ℕ → ℕ) (adversary : Forger) : Forger

Wrap an adaptive forger so that it issues at most one external signing query.

theorem Cslib.Crypto.SignatureScheme.isOraclePPT_limitToOneQuery {bound : ℕ → ℕ → ℕ} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : ℕ × ℕ) => bound p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary 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) (limitToOneQuery bound adversary)

theorem Cslib.Crypto.SignatureScheme.EUFCMA.oneTimeEUFCMA {S : SignatureScheme} (h : S.EUFCMA) : S.OneTimeEUFCMA

Full EUF-CMA security implies one-time EUF-CMA security.