Signatures in the random-oracle model

A signature scheme in the random-oracle model ([BS23], Section 13.2.1) signs and verifies with oracle access to a function H : Query → Digest, which the security experiment draws uniformly at random. Signing draws its coins and then runs an OracleComp program against H; verification is a deterministic OracleComp program. The oracle is sampled lazily: each new point gets a uniform answer, remembered in an association list (oracle), so the query and digest types need not be finite beyond the digests.

The existential-unforgeability experiment (eufCmaGame, [BS23], Attack Game 13.1 in its random-oracle version) gives a forger the public key and oracle access to the signer and to H; the forger wins with a valid signature on a message it never asked to have signed. A Forger has explicit coins, drawn first, and is otherwise a deterministic OracleComp program; this is the form in which a forger can be rerun on the same coins, as forking needs. Its signing and hash calls are counted separately (Forger.CallBounded), as security bounds depend on them differently.

These are exact probability laws for one scheme and one forger, with no efficiency claim. The oracle interface is the library's OracleComp; it is meant to be re-expressed in the shared interactive-protocol core of #643 once that core exists.

This interface is separate from the computational Cslib.Crypto.SignatureScheme, which packages word encodings, strict PPT certificates and verification without an oracle. Here the key and signing coins are arbitrary typed laws, and signing and verification share the hash oracle. A computational statement about a scheme of this form needs encodings, an efficient realization of the oracle and resource certificates on top of the exact bound; the two notions are not competing computational interfaces.

Main definitions

• Cslib.Crypto.Protocols.ROMSignature.Scheme: key generation, signing and verification.
• Cslib.Crypto.Protocols.ROMSignature.Forger: a forger with explicit coins.
• Cslib.Crypto.Protocols.ROMSignature.Forger.CallBounded: bounds on a forger's signing and hash calls.
• Cslib.Crypto.Protocols.ROMSignature.oracle: the lazily sampled uniform random oracle.
• Cslib.Crypto.Protocols.ROMSignature.eufCmaGame: the random-oracle EUF-CMA experiment.
• Cslib.Crypto.Protocols.ROMSignature.Scheme.Correct: honest signatures verify.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Sections 13.1 and 13.2.1.

@[reducible, inline]

abbrev Cslib.Crypto.Protocols.ROMSignature.ForgerSpec (M Query Sig Digest : Type) : OracleSpec (M ⊕ Query)

The calls of a forger: a signing call names a message and returns a signature, and a hash call names a point and returns its digest.

structure Cslib.Crypto.Protocols.ROMSignature.Scheme (PK SK M Sig Query Digest : Type) : Type 1

A signature scheme in the random-oracle model, with public keys PK, secret keys SK, messages M, signatures Sig, and oracle H : Query → Digest. Signing first draws coins.

• keyGen : PMF (PK × SK)

  Draw a public key and a secret key.

• SignCoins : Type

  The signer's coins.

• signCoins : SK → M → PMF self.SignCoins

  Draw the signer's coins for a message.

• sign : SK → M → self.SignCoins → OracleComp (fun (x : Query) => Digest) Sig

  Sign, querying the oracle.

• verify : PK → M → Sig → OracleComp (fun (x : Query) => Digest) Bool

  Verify, querying the oracle.

structure Cslib.Crypto.Protocols.ROMSignature.Forger (PK M Sig Query Digest : Type) : Type 1

A forger with explicit coins: it draws its coins, then, given the public key, calls the signer and the oracle and outputs a message and a signature.

• Coins : Type

  The forger's coins.

• coins : PMF self.Coins

  Draw the forger's coins.

• forge : PK → self.Coins → OracleComp (ForgerSpec M Query Sig Digest) (M × Sig)

  Forge, calling the signer and the oracle.

def Cslib.Crypto.Protocols.ROMSignature.signingCost {M Query : Type} : M ⊕ Query → ℕ

A forger's call costs one when it is a signing call.

def Cslib.Crypto.Protocols.ROMSignature.hashCost {M Query : Type} : M ⊕ Query → ℕ

A forger's call costs one when it is a hash call.

def Cslib.Crypto.Protocols.ROMSignature.Forger.CallBounded {PK M Sig Query Digest : Type} (A : Forger PK M Sig Query Digest) (signs hashes : ℕ) : Prop

The forger makes at most signs signing calls and at most hashes hash calls on every path, for every public key and every choice of its coins.

theorem Cslib.Crypto.Protocols.ROMSignature.Forger.CallBounded.isQueryBounded {PK M Sig Query Digest : Type} {A : Forger PK M Sig Query Digest} {signs hashes : ℕ} (h : A.CallBounded signs hashes) (pk : PK) (coins : A.Coins) : (A.forge pk coins).IsQueryBounded (signs + hashes)

A forger making at most signs signing and hashes hash calls makes at most signs + hashes calls.

noncomputable def Cslib.Crypto.Protocols.ROMSignature.oracle {Query : Type} (Digest : Type) [DecidableEq Query] [Fintype Digest] [Nonempty Digest] (q : Query) : StateT (List (Query × Digest)) PMF Digest

The random oracle: a uniform digest for each new point, remembered thereafter.

noncomputable def Cslib.Crypto.Protocols.ROMSignature.handler {PK SK M Sig Query Digest : Type} [DecidableEq Query] [Fintype Digest] [Nonempty Digest] (scheme : Scheme PK SK M Sig Query Digest) (sk : SK) (q : M ⊕ Query) : StateT (List (Query × Digest) × List M) PMF (ForgerSpec M Query Sig Digest q)

Answer a forger's calls: sign with the secret key, recording the message, or query the oracle. Signing and the forger share the oracle.

noncomputable def Cslib.Crypto.Protocols.ROMSignature.eufCmaGame {PK SK M Sig Query Digest : Type} [DecidableEq Query] [Fintype Digest] [Nonempty Digest] [DecidableEq M] (scheme : Scheme PK SK M Sig Query Digest) (forger : Forger PK M Sig Query Digest) : PMF Bool

The random-oracle EUF-CMA experiment ([BS23], Attack Game 13.1): the forger wins with a valid signature, under the same oracle, on a message it never had signed.

def Cslib.Crypto.Protocols.ROMSignature.Scheme.Correct {PK SK M Sig Query Digest : Type} [DecidableEq Query] [Fintype Digest] [Nonempty Digest] (scheme : Scheme PK SK M Sig Query Digest) : Prop

A scheme is correct when every honest signature verifies under the same oracle, from every state of the oracle.