Indexed signature schemes

An indexed signature scheme ([BS23], Definition 14.6) signs pairs (u, msg) of an index u < q and a message. Its security game lets the adversary choose the indices of its signing queries, but never the same index twice; it wins with a valid signature on any pair (u, msg) it never had signed. An indexed scheme is what a stateful signer that never reuses an index needs: Merkle's tree signature uses the index of the next unused leaf ([Mer90], Section 6; [BS23], Section 14.6.4, where the index is a nonce). The index is an explicit input, so the syntax is stateless; the state is the signer's obligation never to repeat an index, which the game enforces.

The definition here differs from [BS23], Definition 14.6, in four labelled ways.

• Signing may be randomized; the source requires deterministic signing.
• Messages are arbitrary bit strings, with no length restriction.
• Instead of forbidding the adversary to repeat an index, the signing oracle refuses a repeated index, and an index u ≥ q, by returning the empty word and recording nothing. Every oracle adversary is therefore admissible.
• A forgery may name any index, whereas the source's message space is {1, …, q} × M. The structure does not require verification to reject an index u ≥ q; the game does. The oracle never signs at such an index, so a forger that finds a valid signature there wins. This strengthens the source notion.

A request to the signing oracle is the word encPair encUnary encBits (u, msg). The oracle reads every word with the total decoder requestDecoder.

Main definitions

• Cslib.Crypto.IndexedForger: adaptive oracle adversary outputting (u, msg, sig).
• Cslib.Crypto.IndexedSignatureScheme: indexed signature scheme with capacity q(n).
• Cslib.Crypto.IndexedSignatureScheme.requestDecoder: the index and message of a request word.
• Cslib.Crypto.IndexedSignatureScheme.indexedSigningOracle, Cslib.Crypto.IndexedSignatureScheme.indexedEufCmaGame, Cslib.Crypto.IndexedSignatureScheme.IndexedEUFCMA: the security game and predicate.

Main results

• Cslib.Crypto.IndexedSignatureScheme.isPPTOn_run_indexedSigningOracle, Cslib.Crypto.IndexedSignatureScheme.isPPTOn_indexedEufCmaGame: strict PPT certificates for running an oracle-PPT forger against the signing oracle, and for the whole game.
• Cslib.Crypto.IndexedSignatureScheme.IndexedEUFCMA.negligible, Cslib.Crypto.IndexedSignatureScheme.IndexedEUFCMA.of_negligible: security as negligible forging probability.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Section 14.6.1 (Definition 14.6) and Section 14.6.4.
• R. C. Merkle, A Certified Digital Signature, Section 6.

@[reducible, inline]

abbrev Cslib.Crypto.IndexedForger : Type

An adaptive indexed forger receives a unary security parameter and a public key, queries a signing oracle on request words encPair encUnary encBits (u, msg), and outputs a candidate (u, msg, sig).

structure Cslib.Crypto.IndexedSignatureScheme : Type

An indexed signature scheme ([BS23], Definition 14.6, with randomized signing and arbitrary-length messages): at security parameter n it signs pairs (u, msg) with u < capacity n, each index at most once. Key generation and signing are strict PPT, verification is deterministic polynomial time, and every honest signature verifies.

• capacity : ℕ → ℕ

  The number q(n) of indices available at security parameter n.

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

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

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

  Sign the message msg at index u with the secret key sk.

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

  Verify a candidate signature sig on the message msg at index u under pk.

• capacity_polyTime : Turing.MultiTapeTM.ComputableInPolyTime self.capacity Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary

  The capacity is computable in polynomial time, so it is polynomially bounded.

• 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.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)) Turing.MultiTapeTM.encBits fun (p : List Bool × ℕ × List Bool) => self.sign p.1 p.2.1 p.2.2

  Signing is uniformly strict PPT in the secret key, the unary index and the message.

• verify_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : 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.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))) Turing.MultiTapeTM.encBool

  Verification is computable in plain polynomial time on (pk, u, msg, sig).

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

  Every signature produced at an index below the capacity, under a supported key pair, is accepted.

def Cslib.Crypto.IndexedSignatureScheme.requestDecoder : Turing.MultiTapeTM.Decoder (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits)

The index and message of a request word: encPair encUnary encBits (u, msg) decodes to (u, msg), and every other word decodes to some pair.

def Cslib.Crypto.IndexedSignatureScheme.indexedSigningOracle (S : IndexedSignatureScheme) (n : ℕ) (sk : List Bool) (request : Unit × List Bool) : StateT (List (ℕ × List Bool)) ProbComp (List Bool)

The indexed signing oracle at security parameter n. Its state lists the signed pairs, most recent first. A request (u, msg) is signed when u < capacity n and u was never used, and then recorded; any other request receives the empty word and changes nothing.

def Cslib.Crypto.IndexedSignatureScheme.indexedEufCmaGame (S : IndexedSignatureScheme) (adversary : IndexedForger) (n : ℕ) : ProbComp Bool

The indexed EUF-CMA experiment: sample (pk, sk) ← keyGen n, run the forger on (n, pk) with the indexed signing oracle, and accept a valid signature on a pair (u, msg) that was never signed.

theorem Cslib.Crypto.IndexedSignatureScheme.isPPTOn_run_indexedSigningOracle (S : IndexedSignatureScheme) {adversary : IndexedForger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (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.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits))) fun (caller : ℕ × List Bool × List Bool) => (OracleComp.interpret (ProbOracleComp.handler (fun (k : ℕ) => StateT.lift (ProbComp.unifFin k)) (S.indexedSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run []

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

theorem Cslib.Crypto.IndexedSignatureScheme.isPPTOn_indexedEufCmaGame (S : IndexedSignatureScheme) {adversary : IndexedForger} (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) adversary) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool (S.indexedEufCmaGame adversary)

The whole indexed EUF-CMA experiment is uniformly strict PPT in its unary security parameter for every oracle-PPT forger.

def Cslib.Crypto.IndexedSignatureScheme.IndexedEUFCMA (S : IndexedSignatureScheme) : Prop

Existential unforgeability of an indexed scheme under adaptive chosen-message attack ([BS23], Definition 14.6, with the differences listed in the module docstring) against uniform strict oracle-PPT forgers.

theorem Cslib.Crypto.IndexedSignatureScheme.IndexedEUFCMA.negligible {S : IndexedSignatureScheme} (h : S.IndexedEUFCMA) (adversary : IndexedForger) (hadversary : Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) adversary) : Negligible fun (n : ℕ) => Game.succProbability (S.indexedEufCmaGame adversary n).eval

Indexed EUF-CMA security gives negligible forging probability for every oracle-PPT forger.

theorem Cslib.Crypto.IndexedSignatureScheme.IndexedEUFCMA.of_negligible {S : IndexedSignatureScheme} (h : ∀ (adversary : ℕ → List Bool → Probability.WordOracleComp Unit (ℕ × List Bool × List Bool)), Probability.IsOraclePPT (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) adversary → Negligible fun (n : ℕ) => Game.succProbability (S.indexedEufCmaGame adversary n).eval) : S.IndexedEUFCMA

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