Equivalence between one-way functions and one-time digital signatures, and necessity for EUF-CMA

This module establishes the foundational reductions connecting one-way functions (OneWay) and uniform digital signature schemes (SignatureScheme):

1. Secure signatures imply one-way functions (SignatureScheme.OneTimeEUFCMA.exists_oneWay, SignatureScheme.EUFCMA.exists_oneWay): for any digital signature scheme S that is existentially unforgeable under one-time (or full adaptive) chosen-message attack, reindexing the seeded key-generation evaluator (seed ↦ (n, (evaluate n seed).1)) across all input lengths via GeneratorReindex.parameter yields a one-way function. Any PPT inverter for this function gives a zero-query PPT forger that recovers a valid secret key for the challenge public key and signs 0^n.
2. Lamport's one-time signature scheme from any one-way function (lamportScheme, OneWay.oneTimeEUFCMA_lamport, OneWay.exists_oneTimeSignature): given any polynomial-time function f : List Bool → List Bool, lamportScheme f samples 2n independent n-bit secret words, publishes their f-images as the verification key, and signs an n-bit message by revealing one secret word per message bit. When f is one-way (OneWay f), lamportScheme f is one-time EUF-CMA secure (OneTimeEUFCMA): any one-time forger must forge a preimage at some pair (i, msg[i]) that was never revealed by the single signing query.
3. Equivalence (exists_oneWay_iff_exists_oneTimeSignature): a one-way function exists if and only if a one-time EUF-CMA secure signature scheme exists.

Together with SignatureScheme.EUFCMA.oneTimeEUFCMA, this establishes the necessity half of Rompel's theorem ((∃ S, S.EUFCMA) → ∃ f, OneWay f) and the one-time sufficiency half ((∃ f, OneWay f) ↔ (∃ S, S.OneTimeEUFCMA)). Upgrading one-time signatures to stateless many-time EUF-CMA signatures from arbitrary one-way functions requires Rompel's construction of universal one-way hash functions and GMR/Merkle authentication trees.

Main definitions

• Cslib.Crypto.lamportKeyGen, lamportSign, lamportVerify, lamportScheme: Lamport's one-time digital signature scheme built from any polynomial-time function f.
• Cslib.Crypto.lamportInverter: reduction inverting f from a one-time forger against lamportScheme f.

Main results

• Cslib.Crypto.SignatureScheme.OneTimeEUFCMA.exists_oneWay: any one-time EUF-CMA secure signature scheme implies the existence of a one-way function.
• Cslib.Crypto.SignatureScheme.EUFCMA.exists_oneWay: any full EUF-CMA secure signature scheme implies the existence of a one-way function.
• Cslib.Crypto.OneWay.oneTimeEUFCMA_lamport: Lamport's scheme constructed from a one-way function is one-time EUF-CMA secure.
• Cslib.Crypto.OneWay.exists_oneTimeSignature: any one-way function implies the existence of a one-time EUF-CMA secure signature scheme.
• Cslib.Crypto.exists_oneWay_iff_exists_oneTimeSignature: equivalence between one-way functions and one-time EUF-CMA secure signature schemes.

References

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

Secure digital signatures imply one-way functions

theorem Cslib.Crypto.SignatureScheme.OneTimeEUFCMA.exists_oneWay {S : SignatureScheme} (hS : S.OneTimeEUFCMA) : ∃ (f : List Bool → List Bool), OneWay f

Any digital signature scheme that is existentially unforgeable under one-time chosen-message attack (OneTimeEUFCMA) implies the existence of a one-way function.

theorem Cslib.Crypto.SignatureScheme.EUFCMA.exists_oneWay {S : SignatureScheme} (hS : S.EUFCMA) : ∃ (f : List Bool → List Bool), OneWay f

Any digital signature scheme that is existentially unforgeable under adaptive chosen-message attack (EUFCMA) implies the existence of a one-way function.

Lamport's one-time signature scheme from any one-way function

noncomputable def Cslib.Crypto.lamportKeyGen (f : List Bool → List Bool) (n : ℕ) : ProbComp (List Bool × List Bool)

Lamport key generation: sample 2n independent n-bit secret words, publish their f-images as the framed public key, and keep the framed secret words as the signing key.

def Cslib.Crypto.lamportSign (sk msg : List Bool) : ProbComp (List Bool)

Lamport signing: decode the secret key into 2n words and, when the message length matches, reveal word 2 * i + msg[i].toNat for each bit position i < msg.length.

def Cslib.Crypto.lamportVerify (f : List Bool → List Bool) (pk msg sig : List Bool) : Bool

Lamport verification: decode the public key into 2n blocks and the signature into n blocks, and check that f (sigWords[i]) = pkWords[2 * i + msg[i].toNat] for every i < msg.length.

theorem Cslib.Crypto.isPPTOn_lamportKeyGen {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (lamportKeyGen f)

theorem Cslib.Crypto.isPPTOn_lamportSign : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits fun (p : List Bool × List Bool) => lamportSign p.1 p.2

theorem Cslib.Crypto.computableTidilyInPolyTime_lamportVerify {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : List Bool × List Bool × List Bool) => lamportVerify f 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

theorem Cslib.Crypto.lamportVerify_lamportSign (f : List Bool → List Bool) (n : ℕ) (keys : List Bool × List Bool) (hkeys : keys ∈ (lamportKeyGen f n).eval.support) (msg : List Bool) (hmsg : msg.length = n) (sig : List Bool) (hsig : sig ∈ (lamportSign keys.2 msg).eval.support) : lamportVerify f keys.1 msg sig = true

noncomputable def Cslib.Crypto.lamportScheme (f : List Bool → List Bool) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : SignatureScheme

Lamport's one-time digital signature scheme built from any polynomial-time function f.

Security reduction for Lamport's one-time signature scheme

noncomputable def Cslib.Crypto.lamportSimKeys (f : List Bool → List Bool) (n j : ℕ) (y : List Bool) : ProbComp (List Bool × List Bool)

Sample the simulated public key and dummy signing key around a challenge y at index j.

theorem Cslib.Crypto.isPPTOn_lamportSimKeys {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) fun (q : (ℕ × List Bool) × ℕ) => lamportSimKeys f q.1.1 q.2 q.1.2

noncomputable def Cslib.Crypto.lamportInverter (f : List Bool → List Bool) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (adversary : Forger) (n : ℕ) (y : List Bool) : ProbComp (List Bool)

Reduction that inverts f on challenge y at security parameter n by embedding y at a uniformly sampled index j < dyadicSize (2 * n). When j < 2 * n, embed y in slot j of a Lamport public key and run a one-time forger; otherwise return the empty word.

theorem Cslib.Crypto.isPPT_lamportInverter {f : List Bool → List Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) {adversary : Forger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) adversary) : Probability.IsPPT Turing.MultiTapeTM.encBits (lamportInverter f hf adversary)

theorem Cslib.Crypto.OneWay.oneTimeEUFCMA_lamport {f : List Bool → List Bool} (hf : OneWay f) : (lamportScheme f ⋯).OneTimeEUFCMA

Lamport's one-time signature theorem: for any one-way function f, lamportScheme f is existentially unforgeable under one-time adaptive chosen-message attack (OneTimeEUFCMA).

theorem Cslib.Crypto.OneWay.exists_oneTimeSignature {f : List Bool → List Bool} (hf : OneWay f) : ∃ (S : SignatureScheme), S.OneTimeEUFCMA

Any one-way function implies the existence of a one-time EUF-CMA secure signature scheme.

theorem Cslib.Crypto.exists_oneWay_iff_exists_oneTimeSignature : (∃ (f : List Bool → List Bool), OneWay f) ↔ ∃ (S : SignatureScheme), S.OneTimeEUFCMA

Equivalence between one-way functions and one-time digital signatures: a one-way function exists if and only if a one-time EUF-CMA secure uniform signature scheme exists.