Cryptographic Patterns

Cryptographic Schemes as Structures

We model cryptographic schemes as Lean structures that bundle algorithms with their required properties:

-- A commitment scheme bundles commit/reveal with correctness
structure CommitmentScheme (M R C : Type*) where
  -- Algorithms
  commit : M → R → C
  reveal : C → R → M

  -- Correctness property
  correct : ∀ m r, reveal (commit m r) r = m

This pattern appears throughout the site:

• Encryption schemes: KeyGen, Encrypt, Decrypt + correctness
• Signature schemes: KeyGen, Sign, Verify + correctness
• Hash functions: Hash + collision resistance definition

Security Properties

Security properties are expressed as propositions. A scheme satisfies a property if we can prove the proposition:

-- Hiding: commitment reveals nothing about the message
def isHiding (scheme : CommitmentScheme M R C) : Prop :=
  ∀ m₁ m₂ : M, ∀ r₁ r₂ : R,
    -- Commitments are indistinguishable
    Indistinguishable (scheme.commit m₁ r₁) (scheme.commit m₂ r₂)

-- Binding: can't reveal to two different messages
def isBinding (scheme : CommitmentScheme M R C) : Prop :=
  ∀ c : C, ∀ m₁ m₂ : M, ∀ r₁ r₂ : R,
    scheme.commit m₁ r₁ = c →
    scheme.commit m₂ r₂ = c →
    m₁ = m₂

Computational Assumptions

Many cryptographic proofs rely on hardness assumptions. We express these as axioms or unproven propositions:

-- The Discrete Logarithm assumption
def DLog_Hard (s : DLSetting) : Prop :=
  ∀ A : Adversary,           -- For any adversary
    Pr[A wins DLog game] ≤ negl  -- Winning probability is negligible

-- A theorem that assumes DLog hardness
theorem schnorr_secure
    (s : DLSetting)
    (hdlog : DLog_Hard s)        -- Assumption!
    : Secure (SchnorrScheme s) := by
  -- Proof uses hdlog...
  sorry

When you see (h : Assumption) as a theorem parameter, the proof relies on that assumption being true.

Game-Based Security

Security is often defined through games between a challenger and adversary:

-- A security game structure
structure SecurityGame (A : Type*) where
  -- The game procedure
  play : A → Bool              -- Adversary plays, wins or loses

  -- Advantage is distance from random guessing
  advantage : A → ℝ

-- Scheme is secure if no adversary has significant advantage
def Secure (game : SecurityGame A) : Prop :=
  ∀ adv : A, game.advantage adv ≤ negligible

Reduction Proofs

The most common proof technique: reduce breaking the scheme to breaking a hard problem.

-- "If you can break Schnorr, you can solve DLog"
theorem schnorr_reduction
    (A : SchnorrAdversary)           -- Adversary against Schnorr
    (hA : A.advantage > ε)           -- With significant advantage
    : ∃ B : DLogAdversary,             -- We can build DLog solver
        B.advantage ≥ f(ε) := by
  -- Construct B using A as a subroutine
  use constructReduction A
  -- Show B has related advantage
  sorry

The structure is always: assume adversary A exists, construct adversary B that uses A, show B's success relates to A's success.

Concrete vs Asymptotic Security

We formalize both styles:

-- Concrete security bound
theorem elgamal_security
    (hddh : DDH_Advantage ≤ ε_ddh)
    : IND_CPA_Advantage ElGamal ≤ ε_ddh := by
  -- Tight reduction!
  sorry

Reading Site Formalizations

When you explore the proofs on this site, look for:

You're Ready!

You now have the Lean knowledge needed to explore the formalizations on this site. Start with the foundations: