crypto

Crypto Primitives and Reductions

For the LatticeCrypto/ directory layout, scheme entry points, and proof-vs-concrete split, see docs/agents/lattice.md.

Crypto Primitive Structures

Asymmetric encryption (AsymmEncAlg)

structure AsymmEncAlg (m : Type → Type u) [Monad m] (M PK SK C : Type) where
  keygen : m (PK × SK)
  encrypt : (pk : PK) → (msg : M) → m C
  decrypt : (sk : SK) → (c : C) → m (Option M)

Symmetric encryption (SymmEncAlg)

structure SymmEncAlg (m : Type → Type u) [Monad m] (M K C : Type) where
  keygen : m K
  encrypt : K → M → m C
  decrypt : K → C → m (Option M)

Signatures (SignatureAlg)

structure SignatureAlg (m : Type → Type v) [Monad m] (M PK SK S : Type) where
  keygen : m (PK × SK)
  sign (pk : PK) (sk : SK) (msg : M) : m S
  verify (pk : PK) (msg : M) (σ : S) : m Bool

For an end-to-end EUF-CMA reduction worked through the framework (Σ-protocol → Fiat-Shamir transform → managed-RO NMA → replay forking → DLog), see Examples/Schnorr/Signature.lean and the Schnorr signature walkthrough. The Schnorr-specific σ-protocol facts that feed in live in Examples/Schnorr/SigmaProtocol.lean.

Commitment schemes (CommitmentScheme)

structure CommitmentScheme (PP M C D : Type) where
  setup : ProbComp PP
  commit (pp : PP) (m : M) : ProbComp (C × D)
  verify (pp : PP) (m : M) (c : C) (d : D) : Bool

Defined in VCVio/CryptoFoundations/CommitmentScheme.lean together with PerfectlyCorrect, PerfectlyHiding, hidingExp, bindingExp, and extractExp. The standard-model binding ≤ keyed-CR ≤ birthday bridge from a KeyedHashFamily lives in VCVio/CryptoFoundations/HashCommitment.lean as bindingAdvantage_toCommitment_le_keyedCRAdvantage.