sigma protocol

[rm720]

Sigma Protocol Theory

Description

This code introduces the Sigma Protocol Theory into the HOL4 library.

Sigma Protocol

The Sigma Protocol is a fundamental cryptographic primitive essential for Zero Knowledge Proofs.

Key Components

• Three-Move Protocol:
  • Prover sends commitment to secret (using randomness)
  • Verifier sends random challenge
  • Prover sends response based on secret and challenge
• Combiners: Extends basic protocol with:

• OR combiner: proves knowledge of one of two statements
• AND combiner: proves knowledge of both statements
• Equality combiner: proves same witness works for both statements

Properties

• Completeness: If the prover knows a witness w where R(w,s) holds for statement s, they always convinces the verifier
• Special Soundness: Two valid responses to different challenges allows extracting the witness
• Honest-Verifier Zero-Knowledge: Protocol reveals nothing to verifiers who follow the protocol honestly

Theorems

Includes proofs for:

• WellFormed_SP: Shows protocol follows basic conditions
• Complete_SP: Proves completeness property
• SpecialSoundness_SP: Demonstrates knowledge extraction
• SimulatorCorrectness_SP: Shows simulation works correctly
• HonestVerifierZeroKnowledge_SP: Proves zero-knowledge property

Motivation

This contribution:

• Provides foundation for cryptographic protocols
• Enables further usage of Sigma Protocols in applications requiring zero-knowledge proofs
• Demonstrates application of abstract algebra library