feat(Cryptography): draft PR for cryptographic protocols and security definitions#404
feat(Cryptography): draft PR for cryptographic protocols and security definitions#404SamuelSchlesinger wants to merge 10 commits intoleanprover:mainfrom
Conversation
Move Symbol typeclass assumptions into SingleTapeTM fields, reducing repeated section-level assumptions. Add core transition lemmas: determinism of TransitionRelation, no_step_from_halt, and reachable_steps_le_halting_steps for bounding chain lengths to halting endpoints. Introduce monotoneEnvelope for running maxima, with proofs of monotonicity, pointwise bounds, and comparison with monotone upper bounds. Add TimeComputable.toMonotone and rewrite TimeComputable.comp to internalize monotonicity handling, removing the external monotonicity parameter from composition. Update PolyTimeComputable.comp accordingly.
…eductions Define the fundamental complexity classes using single-tape Turing machines, namespaced under Cslib.Complexity. Classes/Core.lean: shared language-level definitions Decides and Verifies. Classes/Time.lean: P, NP, CoNP, PNeNP, and foundational results P_subset_NP and NP_subset_CoNP_iff. Classes/Space.lean: OutputsWithinSpace, SpaceBoundedComputable, PSPACE, and P_subset_PSPACE (a TM running in time t uses at most t work cells). Reductions.lean: polynomial-time many-one reductions (PolyTimeReduces), NPHard, NPComplete, with reflexivity, transitivity, downward closure under P, and NPHard.p_eq_np.
…lexity hierarchy Introduces a circuit and formula framework for Boolean computation, along with the NC and AC circuit complexity hierarchies. ## Circuits and Formulas - `Basis`: typeclass for circuit operation sets with arity and evaluation - `Circuit`: DAG-based Boolean circuits with `eval`, `size`, `depth`, `mapOp` - `CircuitFamily`: indexed families for uniform complexity definitions - `Formula`: tree-structured formulas with standard basis (AND, OR, NOT) - Structural measures (`size`, `depth`, `leafCount`, `gateCount`) - Standard basis constructors and `deMorgan` normalization ## Circuit Complexity - `SizeDepth`: languages decidable by bounded-size, bounded-depth circuits - `NC k` / `AC k`: the standard circuit complexity hierarchies - `NC k ⊆ NC (k+1)`, `NC k ⊆ AC k`, `AC k ⊆ NC (k+1)` - `NonUniform.PSlashPoly`: non-uniform polynomial circuits (P/poly) - `PSPACE_class`: space complexity class definition ## References - [Arora, Barak — Computational Complexity: A Modern Approach][AroraB2009]
Introduces foundational discrete probability theory and the General Forking Lemma of Bellare-Neven (2006). ## Discrete Probability - `uniformExpect`: expected value under the uniform distribution - `uniformProb`: probability of an event under the uniform distribution - Key lemmas: linearity, monotonicity, indicator sums, product sampling - `uniformExpect_eval_at_point`: evaluating a random function at a fixed point equals sampling a uniform value ## General Forking Lemma - `forking_lemma`: if an algorithm accepts with probability `acc`, then replaying with fresh randomness at a random fork point succeeds with probability `≥ acc²/q - acc/|H|` - Proved sorry-free from first principles ## References - [Bellare, Neven — Multi-Signatures and a General Forking Lemma][BellareNeven2006] - [Pointcheval, Stern — Security Arguments for Digital Signatures][PointchevalStern2000]
…games, indistinguishability Introduces the foundational framework for game-based cryptographic security definitions. ## Main Definitions - `Negligible` / `PolynomiallyBounded` / `Noticeable`: asymptotic notions - `SecurityGame`: abstract game-based security parameterized by adversary type - `SecurityReduction`: advantage-preserving adversary transformation - `Ensemble` / `PMFEnsemble`: probability distribution families - `CompIndistinguishable` / `StatIndistinguishable`: indistinguishability notions - `PolyTimeDistinguisher`: polynomial-time distinguisher formalization - `OracleInteraction`: stateful multi-query oracle interaction model - `RandomOracle` / `ROM_EUF_CMA_Game`: random oracle model definitions ## Main Results - Negligible closure: `zero`, `neg`, `add`, `mono`, `mul_polyBounded`, `sqrt_nonneg` - `SecurityReduction.secure_transfer`: reductions transfer security - Perfect ⇒ statistical ⇒ computational indistinguishability ## References - [Goldreich — Foundations of Cryptography, Vol. 1][Goldreich2001] - [Katz, Lindell — Introduction to Modern Cryptography][KatzLindell2014] - [Bellare, Rogaway — Random Oracles are Practical][BellareR1993] - [Bellare, Rogaway — Code-Based Game-Playing Proofs][BellareR2006] - [Shoup — Sequences of Games][Shoup2004]
Defines standard cryptographic primitives and their game-based security notions, plus discrete logarithm hardness assumptions. ## Primitives - `EncryptionScheme` with `IND_CPA_Game` and `IND_CCA_Game` - `PRF` / `PRG` with distinguishing security games - `MACScheme` / `SignatureScheme` with `EUF_CMA_Game` - `OWF` with `InversionGame` - `HashFamily` with `CollisionGame` and `SecondPreimageGame` - `CommitmentScheme` with hiding and binding properties ## Hardness Assumptions - `CyclicGroupFamily`: parameterized cyclic group families - `DLog_Game`: discrete logarithm security game - `DLog_Secure`: DLog hardness assumption ## References - [Goldwasser, Micali — Probabilistic Encryption][GoldwasserM1984] - [GGM — How to Construct Random Functions][GGM1986] - [HILL — A PRG from any OWF][HILL1999] - [GMR — Digital Signatures Secure Against CMA][GMR1988] - [BKR — Security of CBC-MAC][BKR2000] - [Rogaway, Shrimpton — Hash-Function Basics][RogawayS2004] - [Damgård — Collision Free Hash Functions][Damgard1987] - [Blum — Coin Flipping by Telephone][Blum1981]
Defines Sigma protocols and their security properties, with concrete instantiations for Schnorr identification and the Fiat-Shamir transform. ## Sigma Protocols - `SigmaProtocol`: three-move interactive proof structure - `SpecialSoundness` / `SpecialHVZK`: security properties - AND/OR combinators (`SigmaAnd`, `SigmaOr`) with security proofs ## Fiat-Shamir Transform - `FiatShamir.toSignatureScheme`: Sigma protocol → signature scheme - Deterministic challenge derivation from hash of (message, commitment) ## Schnorr Protocol - `SchnorrSigma`: Sigma protocol for discrete log relation - `SchnorrSignatureScheme`: Schnorr signatures via Fiat-Shamir - Special soundness and special HVZK proofs ## References - [Fiat, Shamir — How to Prove Yourself][FiatShamir1986] - [Schnorr — Efficient Signature Generation][Schnorr1991] - [Cramer, Damgård, Schoenmakers — Proofs of Partial Knowledge][CDS1994]
Proves concrete security reductions between cryptographic primitives and the Fiat-Shamir ROM security theorem. ## Primitive Reductions - `PRGtoEncryption`: PRG security ⇒ IND-CPA security of PRG-based encryption - `PRFtoEncryption`: PRF security ⇒ IND-CPA security of PRF-based encryption - `PRFtoMAC`: PRF security ⇒ EUF-CMA security of PRF-based MAC - `HashToCommitment`: collision resistance ⇒ binding of hash-based commitments ## Fiat-Shamir ROM Reduction (Boneh-Shoup §19.6) - `fiatShamir_ROM_bound`: concrete bound `ROM-EUF-CMA advantage ≤ √(q · Adv_R + q/|Ch|) + q² · δ` - `fiatShamirReduction`: relation solver from EUF-CMA adversary via forking lemma and special soundness - `fiatShamir_ROM_secure`: asymptotic EUF-CMA security under computational hardness, super-polynomial challenges, and negligible commitment unpredictability - Game-hop chain: ROM → LazyROM → MapGame_Real → MapGame1_HVZK with commitment-collision and HVZK-simulation arguments
- Order Cslib.lean imports alphabetically - Add all bibliography entries cited in new modules - Clean .gitignore (remove personal artifacts, add trailing newline)
- PRG: expand semantic definition with length-extending and deterministic properties - Commitment: bind coins in commit, use keyed hiding game, keyed randomness - Encryption: use OracleInteraction for IND-CPA/CCA adversaries, add PKE keygen+games - HashToCommitment: adapt reduction for keyed randomness - PRGtoEncryption: adapt reduction for OracleInteraction adversary - PRFtoEncryption: adapt reduction for OracleInteraction adversary
|
Could the following project be relevant? |
Oh yeah, this looks great, thanks for sending it. |
|
Seeing this just now - as an active maintainer of VCVio I'd like to hear about your use cases and whether you want to base upon our repo or continue independently. We do plan to integrate more closely with CSlib in the near future |
I am curious if I am covering anything currently uncovered in your work? Specifically, the most exciting theorem proved in this draft PR by far is unforgeability in the random oracle model of Fiat-Shamirized Sigma Protocol transcripts. It is currently unreviewed and I have found bugs, but they have all been fixable so far, so hopefully there is a kernel of correctness inside of the proof. It certainly looks like the proofs I've seen on paper. Everything else in here is somewhat rote and I wouldn't think it'd have much value to you guys. If I can help by transplanting this proof into your work, I would be very happy to do so, though I may continue on my own path separately at the same time by formalizing Katz-Lindell, edition 3, here: http://github.com/SamuelSchlesinger/introduction-to-modern-cryptography. I'm trying to build that one up slowly with review from collaborators so it can become a trusted base for automated cryptography research using AI. |
|
For a bit of context, the reason I chose Fiat-Shamir as my first target is because I work on anonymous credentials in the IETF and we have a lot of constructions based on them in the Privacy Pass working group. |
|
I highly agree on the value of AI in formalization of cryptography, am heavily AI-aded on my work in VCVio, and actively looking for ways to make it as easy as possible for AIs to write formal crypto proofs. VCVio is rapidly expanding and I'm hoping it could be a shared infrastructure layer for all cryptography work - for instance I just added support for an expectation-based relational Hoare logic, expanding the number of examples (formalizing crypto textbooks is very much on my list, glad you've already started), and a good notion of complexity that's suited to crypto proofs (we care about probabilistic algorithms, expected runtime, precise cost of reductions, etc.) All this is to say that I'd love to chat more and develop any missing features in VCVio to support your work. In the future perhaps the library can be renamed to just CryptoLib - though that requires a broader buy-in from the cryptographic community which I'm hoping would happen. |
You might be curious in this PR then: SamuelSchlesinger/complexitylib#1. It is shaping up to be very nice on the eyes.
Yeah, I am definitely interested in a shared vocabulary layer. What do you think of the monolithic package pattern in Lean 4, like "mathlib", "cslib", and now "cryptolib"? As opposed to other programming languages where we tend to have well-factored, modular packages. It strikes me that it is basically unproductive for velocity and agility, which it strikes me will be more and more important as AI plays more and more of a role. |
|
For instance, we might be able to come to consensus literally this evening on a shared interface for X or Y small thing, then finalize a package for it and make it pretty stable going forward. It will be much harder to come to a consensus on "abstractions for all of cryptography" :) |
3 participants
I do not intend to merge this in this current shape, but I figure this draft is a nice way to share what I am up to at least.
There are likely lots of issues here still and this is not a request for a review. This builds off of #400.
Best read commit by commit.